The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory

DOI10.1007/978-1-4020-8926-8_17MaRDI QIDQ3613313zbMATH OpenOpenAlexFDO

Authors Michael Rathjen

Publication date 12 March 2009

Published in Synthese Library (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-1-4020-8926-8_17

zbMATH Keywords

Martin-Löf type theoryconstructive Hilbert program

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Other constructive mathematics (03F65)

Recommendations

• The constructive Hilbert program and the limits of Martin-Löf type theory
• Constructive Mathematics in Theory and Programming Practice
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Constructive Mathematics and Functional Programming (Abstract)
• Universes in type theory. I. Inaccessibles and Mahlo

Cited in

(7)

• Polynomial-time Martin-Löf type theory
• The constructive Hilbert program and the limits of Martin-Löf type theory
• Proof theory of constructive systems: inductive types and univalence
• A construction of non-well-founded sets within Martin-Löf's type theory
• On the strength of dependent products in the type theory of Martin-Löf
• scientific article; zbMATH DE number 1746890 (Why is no real title available?)
• Well-ordering proofs for Martin-Löf type theory

This page was built for publication: The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory

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