# 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