Higher-Order Confluence and Universe Embedding in the Logical Framework
par Gaspard Férey
mercredi, 30 juin 2021 à 10h00
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.
Jury :
- Maribel Fernández - King’s College London - Reviewer
- Nicolas Tabareau - Inria, Nantes - Reviewer
- 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 - PhD supervisor