Lionel Rieg

From September 2016 to August 2018, I am an associate research scientist at Yale university, inside the Flint group.
You can find my CV here.

Previously, I have been:

Real-time CertiKOS

This project aims at adding real-time properties to CertiKOS, a verified muticore OS kernel.
To this end, we extend CertiKOS with required features: RDTSC support, preemptive interrupts, preemptive priority-based scheduling, etc. We also revisit classical results of real time scheduling theory through a formal proof perspective and using the abstractions already provided by CertiKOS (layers) which combines into the concept of virtual time.

Formal Proofs about Robot Swarms

The Pactole project aims at formalizing results about robot swarms in a unified framework. This framework supports both impossibility proofs (for instance, impossibility of gathering on a real line) and proofs of algorithms (for instance, gathering in the plane).

Formal Proofs about the Compilation of Synchronous Languages

I am currently formalizing the compilation of Esterel towards digital circuits, the final objective being to extract a proven compiler, in the style of CompCert.
Another project I am involved in, Vélus, tackles the formalization of the compilation of Lustre towards imperative code, in particular towards CompCert intermediate language Clight.

PhD Work

My PhD thesis.

The research theme of my PhD is Krivine's classical realizability, more precisely the computational content of forcing inside this framework. I have also worked on introducing real numbers inside the KAM (Krivine Abstract Machine).

I have formalized a (classical) proof of herbrand's theorem inside the Coq proof assistant which, after extraction, gives a certified algorithm in the λc-calculus computing herbrand trees. The directory also contains a makefile and a file to optimize realizers during extraction by kextraction.
Since then, I got a proof by forcing which does not use the fan theorem and from which one can extract a realizer thanks to the forcing translation in classical realizability. The crucial ingredient of this proof is the addition of a Cohen real.
This work is published in the CSL 2013 conference, article freely available here.

I also formalized classical realizability in Coq. The underlying machine is a version of the KAM with environments to which I added several extensions like primive integers and rational numbers, real numbers (partly), or non-determinism. It has been tested with Coq v.trunk (14850) because later versions do not support the classical extraction mechanism (kextraction). Foregoing classical extraction, it compiles with Coq v.8.4pl3.

A list of publications.

How to Contact Me