Higher-Order Confluence and Universe Embedding in the Logical Framework by: Gaspard Férey Wednesday 30 June 2021, 10:00 remote
Summary: In the context of the multiplicity of formal systems, it has become a growing need to express formal proofs into a common logical framework. This thesis focuses on the use of higher-order term rewriting to embed complex formal systems in the simple and well-studied lambda-Pi calculus modulo. This system, commonly used as a logical framework, features dependent types and is extended with higher-order term rewriting. We study, in a first part, criteria for the confluence property of higher-order rewrite systems considered together with the usual beta reduction. In the case of left-linear systems, confluence can be reduced to the study of critical pairs which must be provided a decreasing diagram with relation to some rule labeling. We show that in the presence of non-linear rules, it is still possible to achieve confluence if the set of considered terms is layered. We then focus, in a second part, on the encoding of higher-order logics based on complex universe structures. The embedding of cumulativity, a limited form of subtyping, is handled with new rewriting techniques relying on private symbols and allowing some form of proof irrelevance. We then describe how algebraic universe expressions containing level variables can be represented, even in presence of universe constraints. Eventually we introduce an embedding of universe polymorphism as defined in the core logic of the Coq system and prove the correctness of the defined translation mechanism. These results, along with other more practical techniques, allowed the implementation of a translator to Dedukti which was used to translate several sizable Coq developments.
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