{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,4]],"date-time":"2024-01-04T20:20:51Z","timestamp":1704399651268},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T00:00:00Z","timestamp":1365552000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2013,12]]},"abstract":"In a sequence of papers (Krivine 2001; Krivine 2003; Krivine 2009), J.-L. Krivine introduced his notion of classical realisability<\/jats:italic> for classical second-order logic and Zermelo\u2013Fraenkel set theory. Moreover, in more recent work (Krivine 2008), he has considered forcing constructions on top of it with the ultimate aim of providing a realisability interpretation for the axiom of choice.<\/jats:p>The aim of the current paper is to show how Krivine's classical realisability can be understood as an instance of the categorical approach to realisability as started by Martin Hyland in Hyland (1982) and described in detail in van Oosten (2008). Moreover, we will give an intuitive explanation of the iteration of realisability as described in Krivine (2008).<\/jats:p>","DOI":"10.1017\/s0960129512000989","type":"journal-article","created":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T08:26:46Z","timestamp":1365582406000},"page":"1234-1256","source":"Crossref","is-referenced-by-count":8,"title":["Krivine's classical realisability from a categorical perspective"],"prefix":"10.1017","volume":"23","author":[{"given":"THOMAS","family":"STREICHER","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,4,10]]},"reference":[{"key":"S0960129512000989_ref15","unstructured":"Krivine J.-L. (2010) Realizability algebras II: new models for ZF + DC. Avaialable from http:\/\/www.pps.jussieu.fr\/~krivine\/articles\/R_ZF.pdf."},{"key":"S0960129512000989_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00776-4"},{"key":"S0960129512000989_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000057"},{"key":"S0960129512000989_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BF01792986"},{"key":"S0960129512000989_ref7","first-page":"149","article-title":"Programming with proofs","volume":"26","author":"Krivine","year":"1990","journal-title":"Journal of Information Processing and Cybernetics\/Elektronische Informationsverarbeitung und Kybernetik"},{"key":"S0960129512000989_ref6","first-page":"165","article-title":"The effective topos","volume":"110","author":"Hyland","year":"1982","journal-title":"Proceedings of the The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981)"},{"key":"S0960129512000989_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004106009352"},{"key":"S0960129512000989_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"S0960129512000989_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511605321.003"},{"key":"S0960129512000989_ref16","volume-title":"Realizability: An Introduction to its Categorical Side","author":"van Oosten","year":"2008"},{"key":"S0960129512000989_ref13","article-title":"Realizability in classical logic","volume":"27","author":"Krivine","year":"2009","journal-title":"Interactive models of computation and program behaviour"},{"key":"S0960129512000989_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004107000400"},{"key":"S0960129512000989_ref8","volume-title":"Lambda-calcul, types et mod\u00e8les","author":"Krivine","year":"1990"},{"key":"S0960129512000989_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003141"},{"key":"S0960129512000989_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004102006424"},{"key":"S0960129512000989_ref14","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:2)2011"},{"key":"S0960129512000989_ref12","unstructured":"Krivine J.-L. (2008) Structures de r\u00e9alisabilit\u00e9, RAM et ultrafiltre sur N. Avaialable from http:\/\/www.pps.jussieu.fr\/~krivine\/Ultrafiltre.pdf."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000989","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T02:27:27Z","timestamp":1555986447000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000989\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,10]]},"references-count":17,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["S0960129512000989"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000989","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,10]]}}}