Coq en Coq

Abstract : The essential step of the formal verification of a proof-checker such as Coq is the verification of its kernel: a type-checker for the Calculus of Inductive Constructions (CIC) which is its underlying formalism. The present work is a first small-scale attempt on a significative fragment of CIC: the Calculus of Constructions (CC). We formalize the definition and the metatheory of (CC) in Coq. In particular, we prove strong normalization and decidability of type inference. From the latter proof, we extract a certified Caml Light program, which performs type inference (or type-checking) for an arbitrary typing judgement in CC. Integrating this program in a larger system, including a parser and pretty-printer, we obtain a stand-alone proof-checker, called CoC, for the Calculus of Constructions. As an example, the formal proof of Newman's lemma, build with Coq, can be re-verified by CoC with reasonable performance.
Type de document :
Rapport
[Research Report] RR-3026, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073667
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:26:54
Dernière modification le : samedi 17 septembre 2016 - 01:27:34
Document(s) archivé(s) le : dimanche 4 avril 2010 - 22:05:15

Fichiers

Identifiants

  • HAL Id : inria-00073667, version 1

Collections

Citation

Bruno Barras. Coq en Coq. [Research Report] RR-3026, INRIA. 1996. 〈inria-00073667〉

Partager

Métriques

Consultations de la notice

193

Téléchargements de fichiers

197