Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice

Abstract : Automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. DEDUKTI is such a proof checker. It implements a type system, the lambda-Pi-Calculus Modulo, that is an extension of the dependently-typed lambda-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, DEDUKTI implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in DEDUKTI theorems proved using other tools such as COQ, HOL or ZENON, a first step towards creating interoperability between these systems.The lambda-Pi-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (i.e., the stability of typing by reduction) and uniqueness of types are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guaranteeing the coherence of the proof system, but also for provingthe soundness and completeness of the type-checking algorithms implemented in DEDUKTI. Unfortunately, these properties are undecidable. In this thesis, we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in DEDUKTI.For this purpose, we give a new definition of the lambda-Pi-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that we call product compatibility and well-typedness of rewrite rules.Hence, we study these two properties separately and give effective sufficient conditions for them to hold.These ideas have been implemented in DEDUKTI, increasing its generality and reliability.
Document type :
Theses
Complete list of metadatas

Cited literature [77 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-01299180
Contributor : Abes Star <>
Submitted on : Thursday, April 7, 2016 - 12:12:09 PM
Last modification on : Monday, November 12, 2018 - 11:02:56 AM
Long-term archiving on : Friday, July 8, 2016 - 12:40:49 PM

File

2015ENMP0027_archivage.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01299180, version 1

Citation

Ronan Saillard. Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. Systems and Control [cs.SY]. Ecole Nationale Supérieure des Mines de Paris, 2015. English. ⟨NNT : 2015ENMP0027⟩. ⟨tel-01299180⟩

Share

Metrics

Record views

589

Files downloads

414