research

I am in the programming languages research group at the University of Illinois. One common philosophy underlying most of my research is that statically-typed languages are good. Not only does it eliminate possibly expensive run-time typechecking, type declarations also make programs much clearer to read. The tradeoff is that compile-time typechecking is usually too conservative, and some legal programs would be deemed incorrect. Hence, languages like C++ and Java provide facilities for run-time type information and dynamic typechecking.

 

Syntactic Control of Interference

One of my research projects involves SCI, or Syntactic Control of Interference, which was invented by John Reynolds way back in 1978. SCI is a method for controlling interference, or making sure that different parts of a program don't try to read and write the same memory locations in a way that would cause confusion and chaos. Ensuring noninterference makes it much easier to prove properties about programs. In particular, it has significant implications for concurrent programming.

SCI controls interference based on the program's syntax, so it is possible to devise a set of typing rules to determine when interference may occur. Two type systems for SCI are SCI2, due to Reynolds himself, and SCIR, which was designed by O'Hearn et al. The latter type system is the simpler of the two, but at the time of its invention, it wasn't clear if type inference or even typechecking was feasible. My advisor, Uday Reddy, and I co-wrote a paper entitled Type Reconstruction for SCI which shows that type inference (and hence typechecking) is in fact decidable for SCIR.

In more recent work, we integrated some ideas of Professor Reddy and Hongseok Yang to produce a "better" type inference algorithm, which is documented in Type Reconstruction for SCI, Part 2. This time, some extraneous operators are removed from the language, and we also consider adding let-based polymorphism as in ML.

Object-Oriented Type Systems

Another project involves finding more expressive type systems for object-oriented languages. We would like a language that is "dynamic" like Smalltalk, but still statically-typed like C++ and Java. An ideal type system might have the following features:

• Classes and interfaces should be distinct. The type of an object should be an interface, which only includes information about what methods the object can respond to, and not information about the actual implementation of the object, which is contained in a class. Using classes as types forces recompilation of client code every time a class changes, even if the clients themselves do not change.
  Although Smalltalk is a dynamically-typed language, its concept of typing follows the above approach: two objects which have the same "interface" may be substituted for one another. Java includes both interfaces and classes, but they are both considered types. There are proposals for adding signatures to C++, which would give C++ some of the flavor of Java. In addition, C++ and Java both support pure abstract classes, which are very similar to interfaces.
• Subtyping should be structural, instead of declared. In other words, the programmer should not need to explicitly declare that one interface is a subtype of another, as in Java or C++.
• Separately-compilable parameterized methods, interfaces and classes should be supported. This is particularly important for defining and manipulating container objects, such as linked lists and trees. C++ template compilation requires code substitution, which precludes separate compilation and usually results in overly large object files. Java does not support any notion of parameterization, although proposals for such an extension have been made in projects such as Pizza and PolyJ.
• Binary methods are methods in some class C which expect a parameter of "type" C. Comparison methods, for example, are often implemented as binary methods. Most languages require the use of run-time type information to support such methods, but it is possible to add either F-bounded polymorphism or matching to the type system instead.