I am interested, broadly speaking, in finding out what programs are supposed to be doing, and proving that they actually do what they are supposed to do. In this interplay of specification and verification, I bring to bear ideas and techniques from the fields of logic, programming language theory, type theory, automated deduction and mechanized theorem proving.
Specifically, here are some projects I have been involved in:
Recently, I have been trying to formalize the memory consistency behaviour of machine code on real multiprocessor architectures, including (so far) the x86, Power and ARM architectures. This should serve as a solid foundation for verifying low-level concurrent code. See the weak memory project website for more details.
Before this, my thesis work was in “foundational certified code”, the idea that we formalize low-level semantics of machine code, and directly prove programs safe on this semantics. This is usually done by a very low-level type system, aka typed assembly language. I was involved in proving the soundness of one such type system, called TALT. Along the way, I defined a new dependently-typed program language where very expressive specifications were written out explicitly as types.
Among the other projects I have been involved in, I have used, and in a minor way, developed, the proof assistant Twelf, and formalized and used the general proof assistant front-end Ott.
A bibliography (bibtex) of the papers I have written.
In Feb 2007, I gave a Theory Mini Course on Twelf, a system aimed at specifying, implementing, and proving properties of deductive systems, in particular, programming languages and logics. Materials for the course may be found here.
At Cambridge, I have supervised Types (a part II course) for the Computer Laboratory.
At Carnegie Mellon University, I served as a teaching assistant for 15-399 (Constructive Logic, a junior/senior year course), and 15-251 (Great Ideas in Theoretical Computer Science, a sophomore year course).
Jade Alglave, Thomas Braibant, Karl Crary, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Brigitte Pientka, Tom Ridge, Peter Sewell, Rok Strniša