The generalised type-theoretic interpretation of constructive set theoryCitation formats

  • Authors:
  • Nicola Gambino
  • Peter Aczel

Standard

The generalised type-theoretic interpretation of constructive set theory. / Gambino, Nicola; Aczel, Peter.

In: The Journal of Symbolic Logic, Vol. 71, No. 1, 03.2006, p. 67-103.

Research output: Contribution to journalArticle

Harvard

Gambino, N & Aczel, P 2006, 'The generalised type-theoretic interpretation of constructive set theory' The Journal of Symbolic Logic, vol. 71, no. 1, pp. 67-103. https://doi.org/10.2178/jsl/1140641163

APA

Gambino, N., & Aczel, P. (2006). The generalised type-theoretic interpretation of constructive set theory. The Journal of Symbolic Logic, 71(1), 67-103. https://doi.org/10.2178/jsl/1140641163

Vancouver

Gambino N, Aczel P. The generalised type-theoretic interpretation of constructive set theory. The Journal of Symbolic Logic. 2006 Mar;71(1):67-103. https://doi.org/10.2178/jsl/1140641163

Author

Gambino, Nicola ; Aczel, Peter. / The generalised type-theoretic interpretation of constructive set theory. In: The Journal of Symbolic Logic. 2006 ; Vol. 71, No. 1. pp. 67-103.

Bibtex

@article{a31cce4500164a1eb24131c4fbfc9bd0,
title = "The generalised type-theoretic interpretation of constructive set theory",
abstract = "We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-L{\"o}f type theory. The original interpretation treated logic in Martin-L{\"o}f type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-L{\"o}f type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation. {\circledC} 2006, Association for Symbolic Logic.",
keywords = "Constructive Set Theory, Dependent Type Theory",
author = "Nicola Gambino and Peter Aczel",
year = "2006",
month = "3",
doi = "10.2178/jsl/1140641163",
language = "English",
volume = "71",
pages = "67--103",
journal = "The Journal of Symbolic Logic",
issn = "0022-4812",
publisher = "Cambridge University Press",
number = "1",

}

RIS

TY - JOUR

T1 - The generalised type-theoretic interpretation of constructive set theory

AU - Gambino, Nicola

AU - Aczel, Peter

PY - 2006/3

Y1 - 2006/3

N2 - We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation. © 2006, Association for Symbolic Logic.

AB - We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation. © 2006, Association for Symbolic Logic.

KW - Constructive Set Theory

KW - Dependent Type Theory

U2 - 10.2178/jsl/1140641163

DO - 10.2178/jsl/1140641163

M3 - Article

VL - 71

SP - 67

EP - 103

JO - The Journal of Symbolic Logic

JF - The Journal of Symbolic Logic

SN - 0022-4812

IS - 1

ER -