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.
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.
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: