Karl Crary

Research Statement

My research interests are in the design and implementation of advanced programming languages and in applying programming language technology to improve the development, maintenance, and performance of software systems. I am particularly interested in the application of types to the structure and implementation of programming languages and software systems.

One current focus of my research is on mechanized metatheory. The aim of mechanized metatheory is to give proof of the properties of programming languages (for example, the type safety property says that no well-typed program can crash or otherwise violate its interface) in a form that can be checked by a computer. Not only does this give us greater confidence of the correctness of our proofs, but it also makes it possible for the proof itself to become part of a software system.

For example, we can use mechanized metatheory to provide a form of certified code. By equipping a program with a proof of type safety for the language it is provided in (this may be a source or executable language), we make it possible to determine the safety of the program automatically, simply by checking the proof and type-checking the program. Thus it is feasible to check the safety of programs in a purely automated fashion.

Another current focus of my research is on the application of certified code to operating systems.  Using certified code, we can replace the dynamic protection checks that are ubiquitous in systems today with purely static ones. Since dynamic checks can be unreliable and costly, this can improve the reliability and performance of software systems.  Moreover, static checks have greater expressive power than dynamic checks, so they can offer a greater level of protection and security than existing means.

Publications