Vincent Rahli


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 ML-like 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 Heriot-Watt University in Edinburgh. My supervisors were Professor Fairouz Kamareddine and Doctor J. B. Wells of the ULTRA group.





Papers
Conference papers
Journal papers
Workshop papers
Technical reports




Talks


Interests

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 cyber-physical 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 ML-like 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 correct-by-construction asynchronous protocols.

Synthesis and verification of distributed protocols
Using EventML, we have specified, synthesized, and verified safety properties of the Multi-Paxos 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 Red-Hat-based systems as well as a web demo.



In addition to the Skalpel project, during my PhD I was involved in the following projects:

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.



Thesis and reports


Tutoring and Guest Lectures


Activities


Reviewing


Cool Stuff


Contact
Email (λx.firstname x lastname at uni x lu)dot
Address Luxembourg University
Maison du Nombre
6, Avenue de la Fonte
L-4364 Esch-sur-Alzette
Phone (+352) 46 66 44 6126



Last updated: Apr. 28, 2017