Soutenance de thèse: Gaspard Férey
J'ai le plaisir de vous inviter à assister à ma soutenance de thèse, qui aura lieu le
mercredi 30 juin à 10h
La soutenance se tiendra surtout via l'outil de visio BBCollab.
Titre : Confluence d'ordre supérieur et encodage d'univers dans le Logical Framework
Le jury est composé de :
- Maribel Fernández - King’s College London - Rapporteure
- Nicolas Tabareau - Inria, Nantes - Rapporteur
- Véronique Benzaken - Université Paris Saclay
- Femke van Raamsdonk - Vrije Universiteit, Amsterdam
- Tobias Nipkow - Université Technique de Munich
- Jean-Pierre Jouannaud - Université Paris Saclay
- Gilles Dowek - Inria & ENS Paris-Saclay - Directeur de thèse
Résumé :
La multiplicité des systèmes formels a mis en évidence la nécessité d'un socle logique commun dans lequel les formalismes logiques pourraient être exprimés. L'enjeu principal de ce manuscrit est la définition de techniques d'encodages reposant sur la réécriture de termes et capables de représenter les fonctionnalités avancées des systèmes de types modernes. Nos encodages s'appuieront sur le lambda-Pi calcul modulo, un système de types dépendants, communément utilisé comme socle logique, étendu ici par de la réécriture d'ordre supérieur. On s'intéresse, dans une première partie, aux critères de confluence de systèmes de réécriture avec la bêta réduction. La confluence d'un système linéaire à gauche se déduit de l'étude de ses paires critiques pour lesquelles il faut exhiber un diagramme décroissant vis-à- vis d'un certain étiquetage des règles. Le cas non-linéaire nécessite, lui, une compartimentalisation des termes considérés. On considère, dans un second temps, l'encodage de systèmes de types complexes. Sont étudiés successivement, la cumulativité qui nécessite de considérer des symboles privés pour encoder une forme de "proof irrelevance", les expressions algébriques d'univers sous contraintes d'univers et enfin le polymorphisme d'univers dont on prouve la correction d'une fonction de traduction depuis un sous-ensemble de Coq. L'implantation de ces résultats a permis de traduire en Dedukti plusieurs développements Coq de taille significative.