Research Projects (Revised January 2007)

Mechanizing Language Definitions and Metatheory:

Here at CMU, we use LF and Twelf to mechanize the definitions and metatheory of the languages we design. I've written two introductions to LF and Twelf. The first is a survey article that describes LF and Twelf in technical detail. The second is more tutorial; it is now part of the Twelf Wiki. Read the former if you just want a big-picture sense of what's going on; read the latter (and maybe the former, too) if you actually want to use Twelf.

I have also worked on a module system for Twelf.

Expressive and Practical Dependent Types:

Type systems for current languages such as Standard ML and Haskell can verify important sine qua non program properties; however, there are many crucial properties that these type systems cannot check. Dependent types allow the specification and verification of these more advanced properties, and languages such as Epigram, ATS, and Omega have begun to integrate forms of dependent types into their type systems. The key challenge such languages face is to provide the expressive power of dependent types, so that a programmer can specify and verify the properties important to her program, without sacrificing effective type checking or radically departing from the functional-programming style. We have some preliminary thoughts on how to do this.

Verifying Interactive Web Programs:

Programs that interact with their users through the Web are prone to subtle errors; many of these bugs result from developers failing to account for the Back button and other browser operations. At Brown, I worked with Shriram Krishnamurthi to design a model checker that verifies properties of interactive Web programs.