{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T06:16:17Z","timestamp":1775628977053,"version":"3.50.1"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T00:00:00Z","timestamp":1441843200000},"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":[[2017,3]]},"abstract":"<jats:p>We propose the new concept of<jats:italic>Krivine ordered combinatory algebra<\/jats:italic>(<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129515000432_inline1\"\/><jats:tex-math>$\\mathcal{^KOCA}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013).<\/jats:p><jats:p>We show that<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129515000432_inline1\"\/><jats:tex-math>$\\mathcal{^KOCA}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>'s are equivalent to Streicher's<jats:italic>abstract Krivine structures<\/jats:italic>for the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class of<jats:italic>triposes<\/jats:italic>. The difference between the two representations is that the elements of a<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129515000432_inline1\"\/><jats:tex-math>$\\mathcal{^KOCA}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>play both the role of truth values and realizers, whereas truth values are<jats:italic>sets<\/jats:italic>of realizers in<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129515000432_inline2\"\/><jats:tex-math>$\\mathcal{AKS}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>s.<\/jats:p><jats:p>To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129515000432_inline1\"\/><jats:tex-math>$\\mathcal{^KOCA}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, which showcases the dual role that is played by the elements of the<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129515000432_inline1\"\/><jats:tex-math>$\\mathcal{^KOCA}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1017\/s0960129515000432","type":"journal-article","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T03:19:21Z","timestamp":1441855161000},"page":"428-458","source":"Crossref","is-referenced-by-count":6,"title":["Ordered combinatory algebras and realizability"],"prefix":"10.1017","volume":"27","author":[{"given":"WALTER FERRER","family":"SANTOS","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JONAS","family":"FREY","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MAURICIO","family":"GUILLERMO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"OCTAVIO","family":"MALHERBE","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ALEXANDRE","family":"MIQUEL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,9,10]]},"reference":[{"key":"S0960129515000432_ref8","first-page":"165","volume-title":"The effective topos","author":"Hyland","year":"1982"},{"key":"S0960129515000432_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0960129515000432_ref1","volume-title":"Boolean-valued models and independence proofs in set theory","author":"Bell","year":"1977"},{"key":"S0960129515000432_ref19","unstructured":"Krivine J.L. (2009) Realizability in classical logic in Interactive models of computation and program behaviour, Panoramas et synth\u00e8ses 27 (2009), SMF."},{"key":"S0960129515000432_ref26","doi-asserted-by":"crossref","unstructured":"Streicher T. (2013) Krivine's Classical Realizability from a Categorical Perspective, Math. Struct. in Comp. Science. vol. 23, n 6.","DOI":"10.1017\/S0960129512000989"},{"key":"S0960129515000432_ref10","volume-title":"Sketches of an elephant: a topos theory compendium. Vol. 1","author":"Johnstone","year":"2002"},{"key":"S0960129515000432_ref28","volume-title":"Realizability, an Introduction to its Categorical Side","author":"van Oosten","year":"2008"},{"key":"S0960129515000432_ref13","doi-asserted-by":"crossref","unstructured":"Kleene S.C. (1945) On the interpretation of intuitionistic number theory., Journal of Symbolic Logic, 10:109\u2013124.","DOI":"10.2307\/2269016"},{"key":"S0960129515000432_ref12","doi-asserted-by":"crossref","unstructured":"Hofstra P. and van Oosten J. (2004) Ordered partial combinatory algebras, Math. Proc. Cambridge Philos. Soc. 134, no. 3, pp. 445\u2013463.","DOI":"10.1017\/S0305004102006424"},{"key":"S0960129515000432_ref24","doi-asserted-by":"crossref","unstructured":"Myhill J. (1973) Some properties of intuitionistic Zermelo-Fraenkel set theory, Lecture notes in mathematics 337, pp 206\u2013231.","DOI":"10.1007\/BFb0066775"},{"key":"S0960129515000432_ref16","doi-asserted-by":"crossref","unstructured":"Krivine J.L. (2001) Types lambda-calculus in classical Zermelo-Fraenkel set theory, Arch. Math. Log. 40, no. 3, pp. 189\u2013205.","DOI":"10.1007\/s001530000057"},{"key":"S0960129515000432_ref7","doi-asserted-by":"crossref","unstructured":"Hofstra P. (2008) Iterated realizability as a comma construction, Math. Proc. Cambridge Philos. Soc. 144, no. 1, pp. 39\u201351.","DOI":"10.1017\/S0305004107000400"},{"key":"S0960129515000432_ref17","doi-asserted-by":"crossref","unstructured":"Krivine J.L. (2003), Dependent choice, \u2018quote\u2019 and the clock, Th. Comp. Sc. 308, pp. 259\u2013276.","DOI":"10.1016\/S0304-3975(02)00776-4"},{"key":"S0960129515000432_ref5","doi-asserted-by":"crossref","unstructured":"Griffin T.G. (1990) A Formul\u00e6-as-Types Notion of Control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/96709.96714"},{"key":"S0960129515000432_ref21","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S0960129515000432_ref6","doi-asserted-by":"crossref","unstructured":"Hofstra P. (2006) All realizability is relative, Math. Proc. Cambridge Philos. Soc. 141, no. 2, pp. 239\u2013264.","DOI":"10.1017\/S0305004106009352"},{"key":"S0960129515000432_ref14","doi-asserted-by":"crossref","unstructured":"Krivine J.L. (1994), A general storage theorem for integers in call-by-name lambda-calculus., Th. Comp. Sc., 129, p. 79\u201394.","DOI":"10.1016\/0304-3975(94)90081-7"},{"key":"S0960129515000432_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511542725"},{"key":"S0960129515000432_ref15","doi-asserted-by":"crossref","unstructured":"Krivine J.L. (2001), Realizability algebras: a program to well order $\\mathbb R$ , Logical methods in computer science, vol 7, (3: 02), pp 1\u201347.","DOI":"10.2168\/LMCS-7(3:2)2011"},{"key":"S0960129515000432_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1524-5_4"},{"key":"S0960129515000432_ref23","unstructured":"McCarty D. (1983) Realizability and recursive mathematics, Technical Report CMU-CS-84-131. Departament of Computer Science, Carnegie-Mellon University, 1984. Report version of the author's PhD thesis, Oxford University."},{"key":"S0960129515000432_ref3","first-page":"113","volume-title":"Some applications of Kleene's methods for intuitionistic system","author":"Friedman","year":"1973"},{"key":"S0960129515000432_ref25","volume-title":"Lectures in the Curry\u2013Howard isomorphism","author":"S\u00f8rensen","year":"2006"},{"key":"S0960129515000432_ref9","doi-asserted-by":"crossref","unstructured":"Hyland J.M.E. , Johnstone P.T. and Pitts A.M. (1980) Tripos theory, Math. Proc. Cambridge Phil. Soc. 88, pp 205\u2013232.","DOI":"10.1017\/S0305004100057534"},{"key":"S0960129515000432_ref22","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"S0960129515000432_ref2","volume-title":"Lattice theory","author":"Birkhoff","year":"1955"},{"key":"S0960129515000432_ref18","unstructured":"Krivine J.L. (2008) Structures de r\u00e9alisabilit\u00e9, RAM et ultrafiltre sur $\\mathbb N$ . 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\/S0960129515000432","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,30]],"date-time":"2019-08-30T09:29:48Z","timestamp":1567157388000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129515000432\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,10]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["S0960129515000432"],"URL":"https:\/\/doi.org\/10.1017\/s0960129515000432","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,10]]}}}