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

DOI10.1007/978-1-4020-8926-8_17zbMATH Open1172.03031OpenAlexW2029188589MaRDI QIDQ3613313FDOQ3613313

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

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

zbMATH Keywords

Martin-Löf type theoryconstructive Hilbert program

Mathematics Subject Classification ID

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

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
• Title not available (Why is that?)
• 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)