I will be defending my Ph.D Thesis on November, 20th 2012 at 12:45 . It will take place in the lecture room "Amphithéâtre B" at the third floor of the ENS of Lyon (on the "Jacques Monod" site, see below for instructions to get there).
The thesis was supervised by Patrick Baillot and Olivier Laurent and took place within the plume team of the LIP laboratory. It has been reviewed by Martin Hofmann and Thierry Coquand. And it will be held in front of a Jury is composed by :
This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to build a logic from a programming language, both described as pure type systems. This logic provides formulas to express properties of programs and offers a formal framework that allows us to develop a theory of realizability in which realizers of formulas are exactly programs of the starting programming language. In our framework, the standard representation theorems of Gödel's system T and Girard's system F may be seen as two instances of a more general theorem. Then, we explain how the so-called « logical relations » of parametricity theory may be expressed in terms of realizability, which shows that the generated logic provides an adequate framework for developping a general theory of parametricity. Finally, we show how this parametricity theory can be adapted to the underlying type system of the proof assistant Coq and we give an original example of application of parametricity theory to the formalization of mathematics.