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: