Research Summaries

Implementing certified programming language tools in dependent type theory

My PhD thesis research centered on building programming language tools with proofs of total correctness, using the Coq proof assistant. What distinguishes my approach is that I use dependent types in the implementations of the tools, not just their correctness proofs, following a kind of "correctness by construction" discipline. These are some of the largest dependently-typed programming projects that I'm aware of.

Certified Compilers

My PLDI'07 paper describes a certified type-preserving compiler from lambda calculus to assembly language. This project has also produced a library in support of formalizing programming languages with dependently-typed abstract syntax and denotational semantics.

Certified Program Verifiers

My ICFP'06 paper describes an approach to certified program verifiers. I've developed a component architecture for rapid construction of new certified verifiers for x86 machine code, based on functors for translating verifiers between levels of abstraction.

Proof-carrying code

With George Necula, Evan Chang, and Robert Schneck, I've worked on improving the efficiency of extensible proof-carrying code systems. Our work centers on replacing the transmission and checking of monolithic proofs of program safety with custom, re-usable program analysis tools that justify the trustworthyness of their decisions in different ways. With the Open Verifier project, we proposed a particular online decomposition of proof obligations traditionally encountered in foundational proof-carrying code, guided by a trusted abstract interpretation engine. In our follow-on work on certified verifiers, we instead proposed proving the soundness of program analysis tools once and for all, using a computer proof assistant like Coq.

In both of these projects, I developed complete soundness proofs in Coq for large fragments of x86 Typed Assembly Language.

Interactive computer theorem proving

Most of the research I do today involves some interactive theorem proving. With George Necula, I've worked on making interactive proving easier by creating an interface to George's Nelson-Oppen-style automated theorem prover Kettle. Our implementation supports a novel cooperation mode where a proving task is bounced back and forth between the automated and human provers, as the automated prover identifies useful case splits, discharges some cases automatically, and leaves the rest for the user to prove recursively.

Program analysis

As a summer intern in the Software Productivity Tools group at Microsoft Research Redmond, I worked with my mentor Manuel Fähndrich on the bytecode verifier for the Singularity research operating system. Singularity is novel for its almost total reliance on .NET managed code, even for "systems" code. Static verification of all installed software is a critical part of the Singularity security model, including checking manual memory management and proper adherence to inter-process message-passing protocols. I developed an extensible .NET bytecode verifier and implemented checking for those properties and more.

Software model checking

I've done some implementation work in the BLAST model checker project with Tom Henzinger, Ranjit Jhala, Rupak Majumdar, and Dirk Beyer. I implemented the BLAST specification language, for instrumenting C programs with monitoring code. I added context-free reachability support. I wrote some of the basic support behind automatic model-checking-guided test case generation and combining relational and reachability queries about programs.

Typed compiler intermediate languages

At CMU, I worked with Bob Harper and Leaf Petersen on the TILT type-preserving Standard ML compiler project. I implemented some improvements to some of the intermediate languages, and we developed strict bidirectional type-checking to make type inference more effective on the flattened ML-like terms found in TILT and similar compilers.