Please use this identifier to cite or link to this item:
Title: The generalised type-theoretic interpretation of constructive set theory
Authors: Gambino, Nicola
Aczel, Peter
First Published: Mar-2006
Publisher: Association for Symbolic Logic
Citation: Journal of Symbolic Logic, 2006, 71 (1), pp.67-103
Abstract: 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.
DOI Link: 10.2178/jsl/1140641163
ISSN: 0022-4812
Version: Publisher Version
Status: Peer-reviewed
Type: Article
Rights: Copyright © 2006, Association for Symbolic Logic. Deposited with reference to the publisher’s archiving policy available on the SHERPA/RoMEO website.
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
euclid.jsl.1140641163.pdfPublished (publisher PDF)285.76 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.