Transfinite constructions in classical type theory

DOI10.1007/978-3-319-22102-1_26MaRDI QIDQ2945651zbMATH OpenOpenAlexFDO

Authors Gert Smolka, Steven Schäfer, Christian Doczkal

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

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

Recommendations

• Zermelo’s Well-Ordering Theorem in Type Theory
• scientific article; zbMATH DE number 1302068
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• scientific article; zbMATH DE number 1420782
• Well-ordering proofs for Martin-Löf type theory

Cites work

• Beweisstudien zum Satz von M. Zorn. Herrn Erhard. Schmidt zum 75. Geburtstag gewidmet
• Certifying assembly with formal security proofs: the case of BBS
• Doppelte Hülleninduktion und ein Satz von Hessenberg
• scientific article; zbMATH DE number 1703931 (Why is no real title available?)
• scientific article; zbMATH DE number 3142195 (Why is no real title available?)
• scientific article; zbMATH DE number 3291106 (Why is no real title available?)
• On the Bourbaki-Witt principle in toposes
• Zermelo’s Well-Ordering Theorem in Type Theory

Cited in

(7)

• Transfinite type theory and provability of second order formulas
• Categoricity results for second-order ZF in dependent type theory
• Construction of tame types
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
• Categoricity results and large model constructions for second-order ZF in dependent type theory
• Type reconstruction in F_ω
• Tower induction and up-to techniques for CCS with fixed points

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Transfinite constructions in classical type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945651)