My primary research interest is on using modern type safe languages and proof assistants to build efficient, flexible, and reliable infrastructure (e.g., operating systems, compilers) for future information and communications systems. This includes topics such as programming language design and implementation, advanced development of certified code, interaction of compilers and languages with modern architectures and operating systems, and anything that combines the best of the current language, OS, and architecture research.
Recent progress has demonstrated that modern type safe languages can be implemented efficiently and used in systems and application programming. The results are smaller, better structured, and easier-to-maintain systems. Type safe languages are also ideal for many emerging applications such as extensible operating systems, code migration across the internet (a.k.a., agents), and scripting. For example, type safety and system-wide garbage collection will allow future computer systems to more efficiently utilize system resources and drastically reduce the copying and protection boundary switching---a major bottleneck between fast CPU and networks in today's distributed systems.
I spend most of my time working on the FLINT project. I also collaborated with researchers at U. Chicago and Princeton SIP on the SML/NJ and PCC projects. I'll be teaching CS422 Operating Systems in Spring 2008. In the past I have taught CS112 Introduction to Programming, CS421 Compilers and Interpreters, CS428 Language-Based Security, CS430 Formal Semantics, and CS210 A Second Course in Programming. I also attend the systems seminars on SPAM and APLAR.