Skip to Main content Skip to Navigation

Type Theory and Decision Procedures

Pierre-Yves Strub 1, 2, 3
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : The goal of this thesis is to develop a logical system in which formal proofs of mathematical statements can be carried out in a way which is close to mathematical practice.

Our main contribution is the definition and study of a new calculus, the Calculus of Congruent and Inductive Constructions, an extension of the Calculus of Inductive Constructions (CIC) integrating in its computational part the entailment relation - via decision procedures - of a first order theory over equality. A major technical innovation of this work lies in the computational mechanism: goals are sent to the decision procedure together with a set of user hypotheses available from the current context.

Our main results show that this extension of CIC does not compromise its main properties: confluence, strong normalization, consistency and decidability of proof checking are all preserved (as soon as the incorporated theory is itself decidable). As such, our calculus can be seen as a decidable restriction of the Extensional Calculus of Constructions. It can therefore serve as the basis for an extension of the Coq proof assistant.
Complete list of metadatas

Cited literature [51 references]  Display  Hide  Download
Contributor : Pierre-Yves Strub <>
Submitted on : Monday, January 12, 2009 - 4:57:44 AM
Last modification on : Wednesday, September 16, 2020 - 5:00:15 PM
Long-term archiving on: : Tuesday, June 8, 2010 - 7:22:09 PM


  • HAL Id : tel-00351837, version 1



Pierre-Yves Strub. Type Theory and Decision Procedures. Formal Languages and Automata Theory [cs.FL]. Ecole Polytechnique X, 2008. English. ⟨NNT : 2008EPXX0054⟩. ⟨tel-00351837⟩



Record views


Files downloads