My research is in the design and implementation of programming languages and logics for software verification. More specifically, I am interested in applying programming methodology to facilitate the construction of formal proofs in mathematics in general, and of program correctness in particular. My recent focus has been on designing methods for integrating programming with pointers, concurrency, and other important imperative features, into dependent type systems such as that of the proof assistant Coq. The goal of the integration is to leverage the proving power of Coq to obtain effective and scalable ways for reasoning about security and correctness of imperative programs.

I am also interested in all other aspects of formal mathematics and programming language theory and applications related to compilation, optimization, semantics, interactive theorem proving, program extraction, automated deduction, decision procedures, program analysis and model checking.