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.


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:
  1. the classical realizability library in Coq
  2. a quick formalization of forcing combinators:

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).