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].
Document type :
Master thesis
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-01676409
Contributor : Guillaume Genestier <>
Submitted on : Friday, January 5, 2018 - 3:37:13 PM
Last modification on : Friday, January 4, 2019 - 5:33:35 PM

File

Genestier_RapportLMFI.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

425

Files downloads

141