An interpretation of Martin-löf's type theory in a type-free theory of propositions

Journal of Symbolic Logic 49 (3):730-753 (1984)
  Copy   BIBTEX

Abstract

We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation

Categories

Keywords

Reprint years

DOI

10.2307/2274128

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,174

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 Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
A Construction of Type: Type in Martin-Lof's Partial Type Theory with One Universe.Erik Palmgren - 1991 - Journal of Symbolic Logic 56 (3):1012-1015.
An interpretation of martin‐löf's constructive theory of types in elementary topos theory.Anne Preller - 1992 - Mathematical Logic Quarterly 38 (1):213-240.
Programming in Martin-Löf's Type Theory. An Introduction.Kent Petersson & Jan M. Smith - 1992 - Journal of Symbolic Logic 57 (1):272-274.
The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
The Strength of Martin-Löf's Intuitionistic Type Theory with One Universe.Peter Aczel - 1984 - Journal of Symbolic Logic 49 (1):313-313.
Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality.Geir Waagbø - 1999 - Archive for Mathematical Logic 38 (1):19-60.
Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice.Hajime Ishihara, Maria Emilia Maietti, Samuele Maschio & Thomas Streicher - 2018 - Archive for Mathematical Logic 57 (7-8):873-888.
The independence of peano's fourth axiom from Martin-löf's type theory without universes.Jan M. Smith - 1988 - Journal of Symbolic Logic 53 (3):840-845.

Analytics

Added to PP
2009-01-28

Downloads
84 (#250,231)

6 months
12 (#302,973)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Truth in applicative theories.Reinhard Kahle - 2001 - Studia Logica 68 (1):103-128.
Λ-terms, logic, determiners and quantifiers.Fairouz Kamareddine - 1992 - Journal of Logic, Language and Information 1 (1):79-103.
An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics.Chris Fox & Shalom Lappin - 2004 - Logic Journal of the Interest Group in Pure and Applied Logics 12 (2):135--168.

Add more citations

References found in this work

No references found.

Add more references