PhD Defense: Gaspard Férey
It is my great pleasure to invite you to my PhD defense on
Wednesday, June 30 at 10am
The defense will be held via the visioconference tool BBCollab. In-person attendance at ENS Paris-Saclay will be also possible, under restrictions.
Title: Higher-Order Confluence and Universe Embedding in the Logical Framework
The jury members are:
- 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
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.