Since September 2015, I'm a research associate at the SnT in
Luxembourg, working among other things on the verification
of distributed systems and on intuitionistic type theory.
Check
out my
SnT webpage for more information.
From January 2011 to July 2015, I was a postdoc and then a research associate in the PRL group led by Prof. Robert L. Constable, where I was using and working on the foundations of the Nuprl proof assistant. Here are some of the projects we were working on: The synthesis and verification of distributed protocols specified in the Logic of Events, a logical framework implemented in Nuprl to reason about event orderings (message sequence diagrams). We built EventML, a MLlike specification/programming language that cooperates with Nuprl to specify, synthesize, and verify distributed protocols such as Paxos. We were also implementing Nuprl's PER semantics in Coq. 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. 
Conference papers


Journal papers


Workshop papers


Technical reports

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

Certified theorem proving (KeYmaera X in Coq)
KeYmaera X is a theorem prover for cyberphysical systems (modeled as hybrid systems) that implements a logic called Differential Dynamic Logic (dL for short). KeYmaera X has a small core thanks a uniform substitution based proof calculus. We have implemented and verified this core in Coq. This was joint work with Brandon Bohrer and Andre Platzer from CMU, who have implemented and verified KeYmaera's core in Isabelle. 

Intuitionistic and Nominal Type Theory
Using our formalization of Nuprl in Coq, we are turning Nuprl into an intuitionistic type theory, i.e., we have proved that some versions of Brouwer's continuity and bar induction principles are valid w.r.t. Nuprl's PER semantics. In order to prove the validity of such continuity principles we have turned Nuprl into a nominal type theory. It remains open whether stronger continuity and bar induction rules are also valid. 

EventML
EventML is a MLlike constructive specification language that implements a paradigm for verified programming. It gives precedence to the programming task, and also allows programmers to cooperate with a proof assistant in order to structure arguments of correctness. It is 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 safety properties of the MultiPaxos protocol. To do so, we have automated some patterns of reasoning; and to get efficient code, we have built a process optimizer in Nuprl. We are reusing this methodology to develop other provably correct protocols, striving towards more resilient and trustworthy systems. One of our current goal is to verify Byzantine fault tolerant protocols written in C using, among other things, the Verified Software Toolchain (VST). 

Skalpel
Programming languages such as SML have sophisticated, flexible and safe type systems. Unfortunately, the type error messages for incorrect programs are confusing. Skalpel implements a promising approach to making type errors easier to understand and fix called 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. Check out the web page of our project where you can download packages for Debian and RedHatbased systems as well as a web demo. 
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. 
(λx.firstname x lastname at uni x lu)dot  
Address  Luxembourg University 
Maison du Nombre  
6, Avenue de la Fonte  
L4364 EschsurAlzette  
Phone  (+352) 46 66 44 6126 