Soutenance de thèse de Gaëtan GILBERT (équipe Gallinette)

Gaëtan Gilbert, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « Une théorie des types avec insignifiance des preuves définitionnelle » / « A type theory with definitional proof-irrelevance »

vendredi 20 décembre 2019 à 10h, dans l’amphi Besse de l’IMT-A.

Jury :
Directeur thèse : TABAREAU Nicolas
Co encadrant : SOZEAU Matthieu (CR Inria)
Rapporteurs : ABEL Andreas (Chalmers Techniska Hogskola AB), SPITTERS Bas (Aarhus University)
Autres membres : MAHBOUBI Assia, BERTOT Yves (DR Inria Antipolis), SMOLKA Gert (Saarland University)

Résumé : L’égalité définitionnelle, aussi appelée conversion, pour une théorie des types avec une vérification de type décidable est l’outil le plus simple pour prouver que deux
objets sont les mêmes, laissant le système décider en utilisant uniquement le calcul. Par conséquent, plus il y a de choses égales par conversion, plus il est simple d’utiliser un
langage basé sur la théorie des types. L’insignifiance des preuves, indiquant que deux preuves quelconques de la même proposition sont égales, est une manière possible
d’étendre la conversion afin de rendre une théorie des types plus puissante. Cependant, ce nouveau pouvoir a un prix si nous l’intégrons naïvement, soit en rendant la vérification
de type indécidable, soit en réalisant de nouveaux axiomes—tels que l’unicité des preuves d’identité (UIP)—qui sont incompatibles avec d’autres extensions, comme l’univalence.
Dans cette thèse, nous proposons un moyen général d’étendre une théorie des types avec l’insignifiance des preuves, de manière à ce que la vérification du type soit décidable
et est compatible avec l’univalence. Nous fournissons un nouveau critère pour décider si une proposition peut être éliminée sur un type (en corrigeant et en améliorant la règle
d’élimination des singletons de Coq) en utilisant des techniques provenant de développements récents du filtrage dépendant sans UIP. Nous fournissons aussi une preuve de
la décidabilité du typage à base de relations logiques. Cette extension de la théorie des types a été implementée dans les assistants de preuve Coq et Agda.

Mot-clés : Assistant de preuve, Coq, insignifiance des preuves, univers, UIP

********

Abstract: Definitional equality, a.k.a conversion, for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this thesis, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible 
with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) byusing techniques coming from recent development on dependent pattern matching without UIP. We show the decidability of type checking using logical relations. This extension of type theory has been implemented both in Coq and Agda.

Keywords: Proof assistant, Coq, proof-irrelevance, universes, UIP