Marc Lasson's PhD defense

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 :

Abstract

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.

Manuscript

The manuscript is in French and an non-definitive version may be downloaded.

How to get to the defense ?

The Ecole Normale Supérieure de Lyon is situated in the Gerland area of the 7th district of Lyon, near the Pont Pasteur bridge on the left bank of the Rhône. The Jacques Monod site is located 46 Allée d'Italie, between the Place des Pavillons and the Halle Tony Garnier exhibition centre Access.