Publication details
Transfinite Constructions in Classical Type Theory
Gert Smolka, Steven Schäfer, Christian Doczkal
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Springer-Verlag, 2015
We study a transfinite construction we call tower construction in classical type theory. The construction is inductive and applies to partially ordered types. It yields the set of all points reachable from a starting point with an increasing successor function and a family of admissible suprema. Based on the construction, we obtain type-theoretic versions of the theorems of Zermelo (well-orderings), Hausdorff (maximal chains), and Bourbaki and Witt (fixed points). The development is formalized in Coq assuming excluded middle.
Coq development and slides
Download PDF
Show BibTeX
@INPROCEEDINGS{Transfinite-Constructions-ITP2015,
title = {Transfinite Constructions in Classical Type Theory},
author = {Gert Smolka and Steven Schäfer and Christian Doczkal},
year = {2015},
editor = {Xingyuan Zhang and Christian Urban},
publisher = {Springer-Verlag},
booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} 2015, Nanjing, China, August 24-27, 2015},
series = {LNCS 9236},
}
Login to edit
Legal notice, Privacy policy
