The Strength of Martin-Löf's Intuitionistic Type Theory with One Universe

Journal of Symbolic Logic 49 (1):313-313 (1984)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.2307/2274117

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Review: Peter Aczel, Seppo Miettinen, Jouko Vaananen, The Strength of Martin-Lof's Intuitionistic Type Theory with One Universe. [REVIEW]Wim Veldman - 1984 - Journal of Symbolic Logic 49 (1):313-313.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):446-448.
Extending Martin-Löf Type Theory by one Mahlo-universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.
A general formulation of simultaneous inductive-recursive definitions in type theory.Peter Dybjer - 2000 - Journal of Symbolic Logic 65 (2):525-549.
Inaccessibility in constructive set theory and type theory.Michael Rathjen, Edward R. Griffor & Erik Palmgren - 1998 - Annals of Pure and Applied Logic 94 (1-3):181-200.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
Decidability in Intuitionistic Type Theory is Functionally Decidable.Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):300-304.
Induction–recursion and initial algebras.Peter Dybjer & Anton Setzer - 2003 - Annals of Pure and Applied Logic 124 (1-3):1-47.
Treatise on intuitionistic type theory.Johan Georg Granström - 2011 - New York: Springer.
Constructive notions of set: Part I. Sets in Martin–Löf type theory.Laura Crosilla - 2005 - Annali Del Dipartimento di Filosofia 11:347-387.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.

Analytics

Added to PP
2015-02-05

Downloads
38 (#409,607)

6 months
8 (#342,364)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Interpreting classical theories in constructive ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
Recursive models for constructive set theories.M. Beeson - 1982 - Annals of Mathematical Logic 23 (2-3):127-178.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.

View all 6 citations / Add more citations

References found in this work

No references found.

Add more references