Confluence d'ordre supérieur et encodage d'univers dans le Logical Framework
Gaspard Férey · HAL (Le Centre pour la Communication Scientifique Directe) · 2021
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, criterias for the confluence properties 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 embeding 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 embeding 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 sizeable Coq developments.