Marc Lasson (Cambridge, UK)

Realizability and parametricity in pure type systems and its application to the coq proof assistant

During this talk, I will 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 coq proof assistant. Among many applications, this natural encoding of parametricity inside CIC serves both theoretical purposes (proving the independence of propositions with respect to the logical system) as well as practical aspirations (proving properties of finite algebraic structures, we give an example in finite group theory). This talk will cover topics studied during my PhD thesis and were established in collaboration with Jean-Philippe Bernardy and Chantal Keller.