{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:53:55Z","timestamp":1773096835963,"version":"3.50.1"},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":2841,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2006,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-L\u00f6f type theory. The original interpretation treated logic in Martin-L\u00f6f type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-L\u00f6f 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.<\/jats:p>","DOI":"10.2178\/jsl\/1140641163","type":"journal-article","created":{"date-parts":[[2007,12,19]],"date-time":"2007-12-19T16:22:31Z","timestamp":1198081351000},"page":"67-103","source":"Crossref","is-referenced-by-count":20,"title":["The generalised type-theoretic interpretation of constructive set theory"],"prefix":"10.1017","volume":"71","author":[{"given":"Nicola","family":"Gambino","sequence":"first","affiliation":[]},{"given":"Peter","family":"Aczel","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200006356_ref029","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00012-9"},{"key":"S0022481200006356_ref026","first-page":"153","volume-title":"Logic Colloquium '95","volume":"11","author":"Makkai","year":"1998"},{"key":"S0022481200006356_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.08.002"},{"key":"S0022481200006356_ref039","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1093\/oso\/9780198501275.001.0001","volume-title":"Twenty-five years of Constructive Type Theory","author":"Sambin","year":"1998"},{"key":"S0022481200006356_ref006","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"S0022481200006356_ref038","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00704-1"},{"key":"S0022481200006356_ref035","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1201\/9781439865835-14","volume-title":"Logic colloquium '03","volume":"24","author":"Rathjen","year":"2006"},{"key":"S0022481200006356_ref033","first-page":"1233","volume":"70","author":"Rathjen","year":"2005","journal-title":"The disjunction and related properties for Constructive Zermelo-Frankel Set Theory"},{"key":"S0022481200006356_ref031","first-page":"347","volume":"40","author":"Myhill","year":"1975","journal-title":"Constructive Set Theory"},{"key":"S0022481200006356_ref027","unstructured":"Makkai M. , On comparing definitions of weak n-category, available from the author's web page, 2001."},{"key":"S0022481200006356_ref024","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"S0022481200006356_ref022","unstructured":"Maietti M. E. , The type theory of categorical universes, Ph.D. thesis, Dipartimento di Matematica Pura e Applicata, Universit\u00e0 degli Studi di Padova, 1998, available from the author's web page."},{"key":"S0022481200006356_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BF01278464"},{"key":"S0022481200006356_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.021"},{"key":"S0022481200006356_ref013","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.003.0004"},{"key":"S0022481200006356_ref023","volume-title":"Mathematical Structures in Computer Science","author":"MacLane"},{"key":"S0022481200006356_ref016","first-page":"670","volume":"48","author":"Grayson","year":"1983","journal-title":"Forcing in intuitionistic systems without power-set"},{"key":"S0022481200006356_ref025","unstructured":"Makkai M. , First-order logic with dependent sorts, with applications to category theory, available from the author's web page, 1995."},{"key":"S0022481200006356_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"S0022481200006356_ref005","unstructured":"Aczel P. and Rathjen M. , Notes on Constructive Set Theory, Technical Report 40, Mittag-Leffler Institute, The Swedish Royal Academy of Sciences, 2001, available from the first author's web page at http:\/\/www.cs.man.ac.uk\/~petera\/papers.html."},{"key":"S0022481200006356_ref011","volume-title":"Laurea dissertation","author":"Gambino","year":"1999"},{"key":"S0022481200006356_ref028","volume-title":"Intuitionistic type theory \u2014 Notes by G. Sambin of a series of lectures given in Padua, June 1980","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0022481200006356_ref019","volume-title":"Stone spaces","author":"Johnstone","year":"1982"},{"key":"S0022481200006356_ref030","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00079-3"},{"key":"S0022481200006356_ref034","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.010"},{"key":"S0022481200006356_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061825"},{"key":"S0022481200006356_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"S0022481200006356_ref037","first-page":"87","volume-title":"Mathematical Logic and its Applications","author":"Sambin","year":"1987"},{"key":"S0022481200006356_ref002","first-page":"1","volume-title":"The L. E. J. Brouwer Centenary Symposium","author":"Aczel","year":"1982"},{"key":"S0022481200006356_ref018","volume-title":"Categorical logic and type theory","author":"Jacobs","year":"1999"},{"key":"S0022481200006356_ref003","first-page":"17","volume-title":"Logic, methodology and philosophy of science VII","author":"Aczel","year":"1986"},{"key":"S0022481200006356_ref012","unstructured":"Gambino N. , Sheaf interpretations for generalised predicative intuitionistic systems, Ph.D. thesis, University of Manchester, 2002, available from the author's web page."},{"key":"S0022481200006356_ref036","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200310054"},{"key":"S0022481200006356_ref007","first-page":"1","article-title":"Predicative algebraic set theory","volume":"15","author":"Awodey","year":"2005","journal-title":"Theory and applications of categories"},{"key":"S0022481200006356_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"S0022481200006356_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_1"},{"key":"S0022481200006356_ref009","first-page":"315","volume":"38","author":"Friedman","year":"1973","journal-title":"The consistency of classical set theory relative to a set theory with intuitionistic logic"},{"key":"S0022481200006356_ref010","doi-asserted-by":"publisher","DOI":"10.2307\/1971023"},{"key":"S0022481200006356_ref032","volume-title":"Handbook of Logic in Computer Science","volume":"5","author":"Nordstr\u00f6m","year":"2000"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200006356","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T00:54:00Z","timestamp":1630371240000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200006356\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["S0022481200006356"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1140641163","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6]]}}}