Une théorie des types avec insignifiance des preuves définitionnelle

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 improvingthe so-called singleton elimination of Coq) by using 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.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