Vincent Rahli

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.

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 a ML-like 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 correct-by-construction 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 correct-by-construction protocols.

During my PhD I was involved in the following projects:

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.

Thesis and reports

Tutoring and Lectures



Cool Stuff

Email surname at
Address Cornell University
332 Gates Hall
Computer Science Department
Ithaca, NY 14853
Phone (607) 255 9223

Updated on Apr. 23, 2014