Transfinite Constructions in Classical Type Theory
From MaRDI portal
Publication:2945651
DOI10.1007/978-3-319-22102-1_26zbMath1465.03057MaRDI 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
03F65: Other constructive mathematics
03E20: Other classical set theory (including functions, relations, and set algebra)
03E25: Axiom of choice and related propositions
68V20: Formalization of mathematics in connection with theorem provers
03B38: Type theory
Related Items
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
Uses Software
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