Publication details

Saarland University Computer Science

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               

Login to edit

Legal notice, Privacy policy