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
- by e-mail: firstname.lastname@yale.edu
- by phone: 203-432-2003