Soutenance de thèse de Loïc PUJET
13 décembre 2022 @ 15 h 00 min - 20 h 00 min
Loïc Pujet, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée :
« Computing with extensionality principles in type theory »
Le 13.12.2022 à 15h à la Faculté des Sciences et Techniques, Amphi 34
Jury
– Nicolas Tabareau (directeur de thèse), Inria Rennes
– Thierry Coquand (rapporteur), University of Gothenburg
– Conor McBride (rapporteur), University of Strathclyde
– Jon Sterling, Aarhus University
– Paige North, Utrecht University
– Favonia, University of Minnesota
– Tom Hirschowitz, Université Savoie Mont Blanc
– Ambrus Kaposi, Eötvös Loránd University
Résumé
Dans cette thèse, j’étudie plusieurs manières d’étendre la théorie des types intuitionniste avec des principes d’extensionnalité comme par exemple l’extensionnalité des fonctions ou l’axiome
d’univalence de Voevodsky, tout en préservant les propriétés calculatoires des preuves. Dans une première partie, je développe une méta-théorie complète pour l’égalité observationnelle de Altenkirch et al. J’obtiens notamment une preuve formelle de normalisation, de canonicité et de décidabilité de la conversion pour une théorie des types observationnelle avec des propositions imprédicatives. Dans une seconde partie, j’esquisse une traduction de la théorie des types homotopique vers la théorie des types observationnelle, en me basant sur le modèle cubique de Coquand et al. Enfin dans une dernière partie, j’explique comment tirer parti des propriétés calculatoires de la théorie des types cubique pour obtenir des preuves synthétiques élégantes de résultats classiques de la théorie de l’homotopie, notamment la construction de la fibration de Hopf et le lemme 3×3 pour les sommes amalgamées homotopiques.
Mots clés : Théorie des Types, Assistants à la Preuve, Preuve de Normalisation, Égalité Observationnelle, Théorie Cubique des Types, Homotopie Synthétique.
