Transfinite Constructions in Classical Type Theory

DOI10.1007/978-3-319-22102-1_26zbMath1465.03057OpenAlexW2396379022MaRDI QIDQ2945651

Steven Schäfer, Christian Doczkal, Gert Smolka

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_26

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Other classical set theory (including functions, relations, and set algebra) (03E20) Axiom of choice and related propositions (03E25) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items (4)

Tower Induction and Up-to Techniques for CCS with Fixed Points ⋮ Categoricity results for second-order ZF in dependent type theory ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Certifying assembly with formal security proofs: the case of BBS
• Doppelte Hülleninduktion und ein Satz von Hessenberg
• On the Bourbaki–Witt principle in toposes
• Zermelo’s Well-Ordering Theorem in Type Theory
• Beweisstudien zum Satz von M. Zorn. Herrn Erhard. Schmidt zum 75. Geburtstag gewidmet

This page was built for publication: Transfinite Constructions in Classical Type Theory