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 ML-like 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 Heriot-Watt 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.