Sets in Coq, Coq in Sets
This work is about formalizing models of various type theories of the Calculus of Constructions family. Here we focus on set theoretical models. The long-term goal is to build a formal set theoretical model of the Calculus of Inductive Constructions, so we can be sure that Coq is consistent with the...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2010-01-01
|
| Series: | Journal of Formalized Reasoning |
| Online Access: | http://jfr.cib.unibo.it/article/view/1695/1316 |