Thèse
Here is the whole manuscript in one file (consider the postcript for printing), or you can download the chapters separately:
- Introduction
- Chapter 1: Logic: theory and models
- Chapter 2: The λ-calculus
- Chapter 3: Krivine classical realizability
- Chapter 4: The λµµ̃-calculus
- Chapter 5: The starting point: dPAω
- Chapter 6: Normalization of classical call-by-need
- Chapter 7: A classical sequent calculus with dependent types
- Chapter 8: A sequent calculus with dependent types for classical arithmetic
- Chapter 9: Algebraization of classical realizability
- Chapter 10: Implicative algebras
- Chapter 11: Disjunctive algebras
- Chapter 12: Conjunctive algebras
- Bibliography
Slides
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 http://coq.inria.fr/opam/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 https://gitlab.inria.fr/charguer/tlc.git
git checkout coq-8.6
cd tlc
make
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.