Coq en Coq (version améliorée)
Preuves en Coq
Définition des Termes
Types des noms
Termes en variables nommées
Confluence de CC, Church-Rosser
Métatheorie de CC
Approximations de Types
Candidats de Réductibilité
Interprétation des termes
Interprétation des types
Stabilité de l'interprétation
Théorème de Normalisation Forte
Décidabilité de la Conversion
Décidabilité du Typage
Interface
Extraction
Lemmes Généraux
Résultats Complémentaires sur les Listes
Logique dans Type
Extraction vers les types de Caml
Programmes en Caml
Programme Extrait
Noyau Coc
Exemple: le Lemme de Newman en Coc
Listing de la Preuve
Version de Coq:
Welcome to Coq V6.1 (Dec 24 1996)