Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting - Recherche en informatique (CRI)
 Accéder directement au contenu
Thèse Année : 2020

Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting

Terminaison en présence de types dépendants et encodage par réécriture d’une théorie des types extensionelle avec polymorphisme d’univers

Résumé

Dedukti is a logical framework in which the user encodes the theory she wantsto use via rewriting rules. To ensure the decidability of typing, the rewriting system must be terminating.After recalling some properties of pure type systems and their extension with rewriting, a termination criterion for higher-order rewriting with dependent types is presented. It is an extension of the dependency pairs to the lambda-pi-calculus modulo rewriting. This result features two main theorems. The first one states that the well-foundedness of the call relation defined from dependency pairs implies the strong normalization of the rewriting system.The second result of this part describes decidable sufficient conditions to use the first one. This decidable version of the termination criterion is implemented in “SizeChange Tool”.The second part of this thesis is dedicated to the use of the logical framework Dedukti to encode a rich type theory. We are interested in a fragment of the logic beyond Agda which includes two widely used features: extension of conversion with the eta rule and universe polymorphism.Once again, this work includes a theoretical part, with correct encodings of both features in the lambda-pi-calculus modulo rewriting, and a prototypical translator from Agda to Dedukti.
Dedukti est un cadre logique dans lequel l’utilisateur encode la théorie qu’il souhaite utiliser à l’aide de règles de réécriture. Pour garantir la décidabilité du typage, il faut s’assurer que le système de réécriture utilisé est terminant.Après avoir rappelé les propriétés des systèmes de types purs et leur extension avec de la réécriture, un critère de terminaison pour la réécriture d’ordre supérieur avec types dépendants est présenté. Il s’agit d’une extension de la notion de paires de dépendances au cas du lambda-pi-calcul modulo réécriture. Cerésultat se décompose en deux théorèmes principaux. Le premier stipule que la bonne fondaison de la relation d’appel définie à partir des paires de dépendances implique la normalisation forte du système de réécriture.Le second résultat de cette partie décrit des conditions décidables suffisantes pour pouvoir utiliser le premier théorème. Cette version décidable du critère de terminaison est implémenté dans un outil appelé “SizeChange Tool”.La seconde partie de cette thèse est consacrée à l’utilisation du cadre logiqueDedukti pour encoder une théorie des types riche. Nous nous intéressons plusparticulièrement à la traduction d’un fragment d’Agda incluant deux fonctionnalités très répandues : l’extension de la conversion avec la règle eta et le polymorphisme d’univers.Une fois encore, ce travail possède un versant théorique, avec des encodagesprouvés corrects de ces deux fonctionnalités dans le lambda-pi-calcul modulo réécriture, ainsi qu’une implémentation prototypique de traducteur entre Agda et Dedukti.
Fichier principal
Vignette du fichier
97654_GENESTIER_2020_archivage.pdf (1.48 Mo) Télécharger le fichier
Origine : Version validée par le jury (STAR)

Dates et versions

tel-03167579 , version 1 (12-03-2021)

Identifiants

  • HAL Id : tel-03167579 , version 1

Citer

Guillaume Genestier. Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting. Computation and Language [cs.CL]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG045⟩. ⟨tel-03167579⟩
252 Consultations
300 Téléchargements

Partager

Gmail Facebook X LinkedIn More