You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
E-Book;
Electronic Thesis
Title:
Higher-Order Confluence and Universe Embedding in the Logical Framework ; Confluence d'ordre supérieur et encodage d'univers dans le Logical Framework
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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 répré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 cadre logique, étendu ici par de laréé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. ; 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 ...