a1 Laboratoire de Combinatoire et Informatique Mathématique, Université du Québec à Montréal, Case Postale 8888, Succursale Centre-Ville, Montréal (Québec) H3C 3P8, Canada. E-mail: firstname.lastname@example.org
a2 Schools of Mathematics and Computer Science, University of Manchester, Manchester M13 9Pl, England. E-mail: email@example.com
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.
(Received June 17 2005)
(Accepted October 20 2005)