Here is the whole manuscript in one file (consider the postcript for printing), or you can download the chapters separately:


Here are the slides of my PhD defense.

Coq files

Implicative algebras

A Coq development supports the chapters on algebraic realizability models. Definitions and propositions in PDF directly point to the corresponding files, but you can directly browse the source files here. The whole development can be downloaded here.

This development compiles under Coq 8.6 with Charguéraud TLC library (which has a git branch for 8.6). Coq can be installed through opam (which is probably itself in your favorite distribution repositories):

opam init -n -j 2 # 2 is the number of CPU cores
opam repo add coq-released
opam install coq.8.6 && opam pin add coq 8.6

You might be wanting to install coqide too:

opam install coqide

The TLC library can be installed through the following procedure:

git clone
git checkout coq-8.6
cd tlc
make install

To compile the files, a simple call to the Makefile (make) should do the job. Then you can browse any of the file with CoqIDE or you favorite IDE.

Realizability and λµµ̃-calculus

Inspired from Dagand and Scherer development supporting their paper Normalization by realizability also evaluates, a smaller Coq development illustrates (in the framework of the λµµ̃-calculus) the observation that through the proof of adequacy, the definition of a realizability interpretation induces an operational semantics (Section 4.6). The source is browsable here or downloadable here.