My primary research interest is on using modern 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 lead the Yale FLINT group which aims to build a practical infrastructure for constructing large-scale certified systems software. I also collaborated with researchers at U. Chicago and Princeton SIP on the SML/NJ and PCC projects. I am teaching CS528 Language-Based Security in Spring 2009. In the past I have taught CS112 Introduction to Programming, CS421 Compilers and Interpreters, CS422 Operating Systems, CS430 Formal Semantics, and CS210 A Second Course in Programming. I also attend the systems seminars on SPAM and APLAR.