- A paper describing the formalization (published in the Journal of Formalized Reasoning)
- Download the proofs (.tgz)

- Signatures of IZF
- Introduction/Elimination Rules of IZF Axioms
- Relationnal Replacement Axiom
- Ordered pairs
- Relations and Functions
- Disjoint Sum
- Natural Numbers
- Ordinal Numbers
- Classical Ordinal Numbers
- Fixpoint Theorem
- Grothendieck Universes
- Lambda terms
- Cardinal Numbers
- Semantics of CC in ZF
- Semantics of CCω in Tarski-Grothendieck Set Theory
- Inductive Types Nat and Ord
- Type Theoretical Axiom of Choice
- Model of IZF in Coq
- Building a Grothendieck Universe in Coq
- Skolemization of IZF

- Abstract Models of CC and CCω
- Soundness of Abstract Models of CC
- Mapping CC Syntax to the Abstract Model of CC
- Instantiation of the Abstract Model of CC in HF
- Instantiation of the Abstract Model of CC in IZF
- Soundness of Abstract Models of CCω
- Model of CC with Natural Numbers (with type-based termination for fixpoints)
- Pure Lambda Terms
- Reducibility Candidates and Operations
- Generic Interface of Saturated Sets
- Soundness of Abstract Strong Normalization Models of CC
- Another Proof of Strong Normalization for the Calculus of Constructions

Table of contents of Coq objects