Well-ordering proofs for Martin-Löf type theory
From MaRDI portal
(Redirected from Publication:1295372)
Recommendations
- scientific article; zbMATH DE number 1302068
- Proof theory of Martin-Löf type theory. An overview
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- A coherence theorem for Martin-Löf's type theory
- Zermelo’s Well-Ordering Theorem in Type Theory
- Polynomial-time Martin-Löf type theory
- The constructive Hilbert program and the limits of Martin-Löf type theory
- The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
- Well-Ordering Principles in Proof Theory and Reverse Mathematics
- Publication:4715478
Cites work
- scientific article; zbMATH DE number 3833954 (Why is no real title available?)
- scientific article; zbMATH DE number 432701 (Why is no real title available?)
- scientific article; zbMATH DE number 432702 (Why is no real title available?)
- scientific article; zbMATH DE number 3900744 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- scientific article; zbMATH DE number 4033739 (Why is no real title available?)
- scientific article; zbMATH DE number 4066876 (Why is no real title available?)
- scientific article; zbMATH DE number 4070894 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 193575 (Why is no real title available?)
- scientific article; zbMATH DE number 3494394 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 3532926 (Why is no real title available?)
- scientific article; zbMATH DE number 3556031 (Why is no real title available?)
- scientific article; zbMATH DE number 3572133 (Why is no real title available?)
- scientific article; zbMATH DE number 1088206 (Why is no real title available?)
- scientific article; zbMATH DE number 946307 (Why is no real title available?)
- A new system of proof-theoretic ordinal functions
- A well-ordering proof for Feferman's theoryT 0
- Constructive mathematics and computer programming
- Constructivism in mathematics. An introduction. Volume II
- Die Beziehungen Zwischen den OrdinalzahlsystemenΣ Und $$\bar \Theta \left( \omega \right)$$
- Domain interpretations of Martin-Löf's partial type theory
- How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- On the syntax of Martin-Löf's type theories
- Proof theory. 2nd ed
- The strength of some Martin-Löf type theories
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
Cited in
(28)- scientific article; zbMATH DE number 7401822 (Why is no real title available?)
- Transfinite type theory and provability of second order formulas
- A flexible type system for the small Veblen ordinal
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- Inaccessibility in constructive set theory and type theory
- Transfinite constructions in classical type theory
- The strength of some Martin-Löf type theories
- scientific article; zbMATH DE number 946307 (Why is no real title available?)
- scientific article; zbMATH DE number 5173450 (Why is no real title available?)
- 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
- Proof theory of Martin-Löf type theory. An overview
- From realizability to induction via dependent intersection
- The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
- Ordinal analysis by transformations
- Realization of analysis into Explicit Mathematics
- An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
- On the strength of dependent products in the type theory of Martin-Löf
- Helly's selection theorem and the principle of local reflexivity of ordered type
- Wellfoundedness proofs by means of non-monotonic inductive definitions. II: First order operators
- Universes in explicit mathematics
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- The strength of Martin-Löf type theory with a superuniverse. II
- On Relating Theories: Proof-Theoretical Reduction
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
- Zermelo’s Well-Ordering Theorem in Type Theory
- Universes in type theory. I. Inaccessibles and Mahlo
This page was built for publication: Well-ordering proofs for Martin-Löf type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1295372)
