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