package coq-izf
Intuitionistic Zermelo-Fraenkel Set Theory in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v8.10.0.tar.gz
md5=7c5702e4d615d9cfeb56ca36d1ff0189
Description
This development contains the set-as-pointed-graph interpretation of Intuitionistic Zermelo Frankel set theory in system F_omega.2++ (F_omega + one extra universe + intuitionistic choice operator), which is described in chapter 9 of the author's PhD thesis (for IZ) and in the author's CSL'03 paper (for the extension IZ -> IZF).
On This Page