Formalisation and Meta-Theory of Type Theory

Dans cette these, je parle de la meta-theorie de la theorie des types et de la facon de la formaliser dans un assistant de preuve. Je me concentre d’abord sur une traduction conservative de la theorie des types extensionnelle vers la theorie des types intensionnelle ou faible, entierement ecrite en Coq. La premiere traduction consiste en une suppression de la regle de reflection de l’egalite, tandis que la deuxieme traduction produit quelque chose de plus fort : la theorie des types faibles est une theorie des types sans notion de conversion. Le resultat de conservativite implique que la conversion n’augmente pas la puissance logique de la theorie des types. Ensuite, je montre ma contribution au projet MetaCoq de formalisation et de specification de Coq au sein de Coq. En particulier, j’ai travaille sur l’implantation d’un verificateur de type pour Coq, en Coq. Ce verificateur de type est prouve correct vis a vis de la specification et peut etre extrait en code OCaml et execute independamment du verificateur de type du noyau de Coq. Pour que cela fonctionne, nous devons nous appuyer sur la metatheorie de Coq que nous developpons, en partie, dans le projet MetaCoq. Cependant, en raison des theoremes d’incompletude de Godel, nous ne pouvons pas prouver la coherence de Coq dans Coq, ce qui signifie que certaines proprietes — principalement la forte normalisation — doivent etre supposees, c’est-a-dire prises comme axiomes.