Skip to Main content Skip to Navigation
New interface
Master thesis

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 metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Guillaume Genestier Connect in order to contact the contributor
Submitted on : Friday, January 5, 2018 - 3:37:13 PM
Last modification on : Tuesday, October 25, 2022 - 4:21:20 PM


Files produced by the author(s)


  • HAL Id : hal-01676409, version 1


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⟩



Record views


Files downloads