My manuscript is entitled On Forcing and Classical Realizability.
It is available here
for a color-version and there for a
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.
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.