The generalised type-theoretic interpretation of constructive set theory

Research output: Contribution to journalArticle

  • Authors:
  • Nicola Gambino
  • Peter Aczel


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.

Bibliographical metadata

Original languageEnglish
Pages (from-to)67-103
Number of pages36
JournalThe Journal of Symbolic Logic
Issue number1
Publication statusPublished - Mar 2006