PhD
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 proof by forcing of Herbrand's theorem, 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.
Manuscript
My manuscript is entitled On Forcing and Classical Realizability.
It is available here
for a color-version and there for a
printer-friendly version.
Additional documents are as follows:
- the classical realizability library in Coq
- a quick formalization of forcing combinators:
- here for a forcing structure,
- there for a forcing datatype,
- the common file for both formalizations.
PhD defense
My defense took place on June, 17th, 2014 at 14h30 in
the D amphitheatrum of the ENS de Lyon.
As I was asked for them, here are the slides of my defense
(in French).