Polynomial-time Martin-Löf type theory

Archive for Mathematical Logic 32 (2):137-150 (1992)
  Copy   BIBTEX

Abstract

Fragments of extensional Martin-Löf type theory without universes,ML 0, are introduced that conservatively extend S.A. Cook and A. Urquhart'sIPV ω. A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, some examples in group theory are considered

Categories

Keywords

Reprint years

DOI

10.1007/bf01269954

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,449

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

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.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
Homotopy theoretic models of identity types.Steve Awodey & Michael Warren - 2009 - Mathematical Proceedings of the Cambridge Philosophical Society 146:45–55.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Extensionality Versus Constructivity.Silvio Valentini - 2002 - Mathematical Logic Quarterly 48 (2):179-187.
Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
Characterizing the interpretation of set theory in Martin-Löf type theory.Michael Rathjen & Sergei Tupailo - 2006 - Annals of Pure and Applied Logic 141 (3):442-471.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
Martin-Löf’s Type Theorу: Between Phenomenology and Analytical Philosophy.Oleg Domanov - 2024 - HORIZON. Studies in Phenomenology 13 (1):33-56.

Analytics

Added to PP
2013-11-23

Downloads
34 (#698,174)

6 months
7 (#469,699)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Add more references