PhD

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, here are the slides of my defense.