Type Theory and Decision Procedures - Archive ouverte HAL Access content directly
Theses Year : 2008

Type Theory and Decision Procedures

Théorie des Types et Procédures de Décision

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.
Le but de cette thèse est l'étude d'un système logique formel dans lequel les preuves formelles de propriétés mathématiques sont menées dans un style plus proches des pratiques des mathématiciens.

Notre principal apport est la définition et l'étude du Calcul des Constructions Inductives Congruentes, une extension du Calcul des Constructions Inductives (CIC), intégrant au sein de son mécanisme de calcul des procédures de décisions pour des théories equationnelles au premier ordre.

Nous montrons que ce calcul possède toutes les propriétés attendues: confluence, normalisation forte, cohérence logique et décidabilité de la vérification de types sont préservées. En tant que tel, notre calcul peut être vu comme une restriction décidable du Calcul des Constructions Extentionnelles et peut servir comme base pour l'extension de l'assistant à la preuve Coq.
Fichier principal
Vignette du fichier
manuscrit.pdf (1.01 Mo) Télécharger le fichier
Loading...

Dates and versions

tel-00351837 , version 1 (12-01-2009)

Identifiers

  • HAL Id : tel-00351837 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More