From September 2016 to August 2018, I am an associate research scientist at
Yale university, inside
the Flint group.
Previously, I have been:
This project aims at adding real-time properties
to CertiKOS, a
verified muticore OS kernel.
To this end, we revisit classical results of real time scheduling theory
through a formal proof perspective and using the abstractions already
provided by CertiKOS (layers).
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,
gathering on a real line) and proofs of algorithms
(for instance, gathering in the
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.
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
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
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.
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
Foregoing classical extraction, it compiles with Coq v.8.4pl3.
A list of publications.
How to Contact Me
- by e-mail: firstname.lastname@example.org
- by phone: 203-432-2003