Publication details

Saarland University Computer Science

Hereditarily Finite Sets in Constructive Type Theory

Gert Smolka, Kathrin Stark

Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-27, 2016, Vol. 9807 of LNCS, pp. 374-390, Springer, 2016

We axiomatize hereditarily finite sets in constructive type theory and show that all models of the axiomatization are isomorphic. The axiomatization takes the empty set and adjunction as primitives and comes with a strong induction principle. Based on the axiomatization, we construct the set operations of ZF and develop the basic theory of finite ordinals and cardinality. We construct a model of the axiomatization as a quotient of an inductive type of binary trees. The development is carried out in Coq.

Coq development and slides

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy