Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint

Abstract : Dedukti is a type-checker for the λΠ-calculus modulo theory, which has the particularity to allow the user to declare rewrite rules, especially in order to encode the logic he/she wants to use. Thanks to the Curry-Howard-De Bruijn correspondence, the type checking done by Dedukti can be used to check proofs. Unfortunately, to decide the type-checking, Dedukti needs the system of rewrite rules declared by the user, together with β-reduction, to be confluent and terminating. An external tool already exists to check the confluence, but no automatic tool exists for the termination, which must be checked independently by hand, before using Dedukti. The subject of this report (and more widely of the internship) is to develop such a tool. A first part of it is dedicated to an algorithm of termination checking: the Size-Change Principle. After a brief introduction to Dedukti, the algorithm is explained and the results obtained by an implementation of it for Dedukti are presented. The second and longest part of this report is much more theoretic, since it presents reducibility candidates for the λΠ-calculus modulo theory. Those reducibility candidates can then be used together with the Size-Change Principle detailed in the first part, to check the termination of a rewrite rule system, as explained in [Wah07].
Type de document :
Mémoires d'étudiants -- Hal-inria+
Logic in Computer Science [cs.LO]. 2017
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01676409
Contributeur : Guillaume Genestier <>
Soumis le : vendredi 5 janvier 2018 - 15:37:13
Dernière modification le : jeudi 15 novembre 2018 - 20:27:41

Fichier

Genestier_RapportLMFI.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01676409, version 1

Citation

Guillaume Genestier. Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint. Logic in Computer Science [cs.LO]. 2017. 〈hal-01676409〉

Partager

Métriques

Consultations de la notice

349

Téléchargements de fichiers

84