Coq en Coq

Preuves en Coq

• Définition des Termes
• Confluence de CC, Church-Rosser
• Métatheorie de CC
• Lemme de renforcement
• Approximations de Types
• Squelettes d'Ordres
• Candidats de Réductibilité
• Interprétation des Termes et des Types
• Théorème de Normalisation Forte
• Décidabilité de la Conversion
• Décidabilité du Typage
• Cohérence logique
• Extraction du noyau

Lemmes Généraux

• Résultats Complémentaires sur les Listes

Programmes en Caml

• Programme Extrait
• Noyau Coc

Exemple: le Lemme de Newman en Coc

• Listing de la Preuve