Sets in Coq, Coq in Sets
Downloadable resources:
- A paper describing
the formalization (published in the Journal of Formalized Reasoning)
- Download the proofs (.tgz)
Intuitionistic Zermelo-Fraenkel
Hereditarily Finite Set Theory
Calculus of Constructions
Calculus of Constructions with Universes
Models of the Calculus of Constructions (pure and with universes)
General Purpose Libraries
Table of contents of Coq objects