Since July 2013, I am research associate in the
PRL group led by
Prof. Robert L. Constable.
In the PRL group, we use Nuprl, a proof assistant that
implements CTT, a constructive type theory. Here are some
of the projects we are working on.
We are working on synthesizing and verifying distributed
protocols specified in the Logic of Events, a logical
framework implemented in the Nuprl to reason about event
structures (message sequence diagrams). We have built
EventML,
a MLlike constructive specification language that cooperates with Nuprl to
specify, synthesize, and verify distributed protocols such as Paxos.
We are also implementing Nuprl's PER semantics in Coq. This
will eventually give us a verified version of Nuprl.
From October 2006 to January 2011 I was a PhD student in the School of Mathematical and Computer Sciences at HeriotWatt University in Edinburgh. My supervisors were Professor Fairouz Kamareddine and Doctor J. B. Wells of the ULTRA group. From January 2011 to July 2013 I was a postdoc in the PRL group. 
Conference papers


Journal papers


Workshop papers


Technical reports

Certified theorem proving
Stuart Allen's Partial Equivalence Relation (PER) semantics provides a semantics for Nuprl's type theory and allows one to prove that Nuprl's derivation rules are valid. Until recently these proofs were done by hand. In order to prove that these rules are correct, we have implemented this PER semantics in the Coq proof assistant. This implementation (1) provides a bridge between Nuprl and Coq, and (2) is the basis for building a certified version of Nuprl. 

EventML
EventML a MLlike constructive specification language that illustrates a new paradigm for verified programming. It gives precedence to the programming task, but also allows programmers to cooperate with a proof assistant in order to structure arguments of correctness. It is a designed specifically to cooperate with the Nuprl proof assistant in order to develop correctbyconstruction asynchronous protocols. 

Synthesis and verification of distributed protocols
Using EventML, we have specified, synthesized, and verified the safety properties of the Multi Paxos protocol. In order to support proving that the specification satisfies correctness criteria, we have automated some patterns of reasoning; and to get efficient code, we are building a process optimizer in Nuprl. This methodology can be reused to develop other correctbyconstruction protocols. 
A type error slicer for SML
Programming languages such as SML have sophisticated, flexible and safe type systems. Unfortunately, the type error messages for incorrect programs are confusing. promising approach to making type errors easier to understand and fix is type error slicing, in which slices (program points) containing all and only the information needed by the programmer to understand and fix a type error are identified and exhibited. We provide the following resources concerning our type error slicer:


Semantics of expansion
Intersection types introduce type polymorphism in a finitary way. Expansion was introduced to recover the principal typing property in such systems. The study of realisability semantics for such systems with expansion might help casting some light on the expansion mechanism. 

Reducibility proofs
Reducibility is a method based on realisability semantics where the idea is to interpret types by sets of λterms closed under some properties. This method seems promising in generalising diverse properties' proofs of the (typed or untyped) λcalculus. 
surname at cs.cornell.edu  
Address  Cornell University 
332 Gates Hall  
Computer Science Department  
Ithaca, NY 14853  
Phone  (607) 255 9223 