# 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.

- From the Lyon-Saint Exupéry Airport: Take the Rhône Express from the airport to the Part-Dieu rail station.
- From the Lyon Part-Dieu rail station: Take the Vivier Merle exit of the rail station, then take the subway, line B in the direction of the Stade de Gerland. Get down at the "Debourg" stop. Then follow the way below to get to the ENS.

View Larger Map