Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INPROCEEDINGS{SmolkaStark:2016:Hereditarily,
  title = {Hereditarily Finite Sets in Constructive Type Theory},
  author = {Gert Smolka and Kathrin Stark},
  year = {2016},
  editor = {Jasmin Christian Blanchette and Stephan Merz},
  publisher = {Springer},
  booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP} 2016, Nancy, France, August 22-27, 2016},
  series = {LNCS},
  volume = {9807},
  pages = {374-390},
}

Login to edit