Coq in Coq (enhanced version)
Proofs in Coq
Definition of terms
Type of names
Named Variables terms
Confluence of CC, Church-Rosser
Metatheory of CC
Type approximation
Reducibility Candidates
Interpretation of terms
Interpretation of types
Stability of the interpretation
Strong Normalization Theorem
Decidability of conversion
Decidability of typing
Interface
Extraction
General Lemmas
Additional results on lists
Logic fragment in Type
Extraction towards Caml types
Caml Programs
Extracted program
Kernel of Coc
Example: Newman's lemma in Coc
Proof listing
Coq version:
Welcome to Coq V6.1 (Dec 24 1996)