{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T20:26:28Z","timestamp":1648844788701},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2018,4,26]],"date-time":"2018-04-26T00:00:00Z","timestamp":1524700800000},"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":[[2019,3]]},"abstract":"<jats:p>In this work, we continue our consideration of the constructions presented in the paper<jats:italic>Krivine's Classical Realizability from a Categorical Perspective<\/jats:italic>by Thomas Streicher. Therein, the author points towards the interpretation of the classical realizability of Krivine as an instance of the categorical approach started by Hyland. The present paper continues with the study of the basic algebraic set-up underlying the categorical aspects of the theory. Motivated by the search of a full adjunction, we introduce a new closure operator on the subsets of the stacks of an abstract Krivine structure that yields an adjunction between the corresponding application and implication operations. We show that all the constructions from ordered combinatory algebras to triposes presented in our previous work can be implemented,<jats:italic>mutatis mutandis<\/jats:italic>, in the new situation and that all the associated triposes are equivalent. We finish by proving that the whole theory can be developed using the ordered combinatory algebras with full adjunction or strong abstract Krivine structures as the basic set-up.<\/jats:p>","DOI":"10.1017\/s0960129518000075","type":"journal-article","created":{"date-parts":[[2018,4,26]],"date-time":"2018-04-26T05:08:14Z","timestamp":1524719294000},"page":"430-464","source":"Crossref","is-referenced-by-count":1,"title":["Realizability in ordered combinatory algebras with adjunction"],"prefix":"10.1017","volume":"29","author":[{"given":"WALTER FERRER","family":"SANTOS","sequence":"first","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"}]}],"member":"56","published-online":{"date-parts":[[2018,4,26]]},"reference":[{"key":"S0960129518000075_ref7","doi-asserted-by":"crossref","unstructured":"Griffin T. G. (1990). A Formul\u00e6-as-Types Notion of Control, In: Proceedings of the Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/96709.96714"},{"key":"S0960129518000075_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S0960129518000075_ref2","volume-title":"Handbook of Categorical Algebra Volume 1. Basic Category Theory","author":"Borceux","year":"2008"},{"key":"S0960129518000075_ref16","unstructured":"Krivine J.-L. (2009). Realizability in classical logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et synth\u00e8ses, vol. 27, SMF."},{"key":"S0960129518000075_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004102006424"},{"key":"S0960129518000075_ref15","unstructured":"Krivine J.-L. (2008). Structures de r\u00e9alisabilit\u00e9, RAM et ultrafiltre sur \u2115, Available at http:\/\/www.pps.jussieu.fr\/krivine\/Ultrafiltre.pdf."},{"key":"S0960129518000075_ref25","volume-title":"Realizability, an Introduction to its Categorical Side","author":"van Oosten","year":"2008"},{"key":"S0960129518000075_ref1","volume-title":"Lattice Theory","author":"Birkhoff","year":"1995"},{"key":"S0960129518000075_ref5","unstructured":"Ferrer Santos W. , Guillermo M. and Malherbe O. (2013). A Report on Realizability, arXiv:1309.0706v2 [math.LO], 1\u201325."},{"key":"S0960129518000075_ref4","volume-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"S0960129518000075_ref6","first-page":"1","volume-title":"Ordered Combinatory Algebras and Realizability","author":"Ferrer Santos","year":"2015"},{"key":"S0960129518000075_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004106009352"},{"key":"S0960129518000075_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"S0960129518000075_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00776-4"},{"key":"S0960129518000075_ref17","doi-asserted-by":"crossref","unstructured":"Krivine J.-L. Realizability Algebras: A Program to Well Order R, Logical Methods in Computer Science, vol. 7, Issue 3, 2.","DOI":"10.2168\/LMCS-7(3:2)2011"},{"key":"S0960129518000075_ref18","doi-asserted-by":"crossref","unstructured":"Krivine J.-L. (2012). Realizability algebras II : New models of ZF + DC, Logical Methods in Computer Science, vol. 8, Issue 1, 10.","DOI":"10.2168\/LMCS-8(1:10)2012"},{"key":"S0960129518000075_ref19","first-page":"1","volume-title":"Realizability Algebras III: Some Examples","author":"Krivine","year":"2016"},{"key":"S0960129518000075_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000057"},{"key":"S0960129518000075_ref20","volume-title":"Categories for the Working Mathematician","author":"MacLane","year":"1997"},{"key":"S0960129518000075_ref21","unstructured":"Miquel A. (2014). Implicative Algebras for Noncommutative Forcing, Available at http:\/\/smc2014.univ-lyon1.fr\/lib\/exe\/fetch.php?media=miquel.pdf?"},{"key":"S0960129518000075_ref22","unstructured":"Miquel A. (2016). Implicative Algebras: A New Foundation for Forcing and Realizability, Available at https:\/\/www.pedrot.fr\/montevideo2016\/miquel-slides.pdf"},{"key":"S0960129518000075_ref14","unstructured":"Krivine J.-L. (2004). Realizability in Classical Logic, Lessons in Marseille-Lumini, (revised in 2005), 1\u201329. Available at https:\/\/hal-univ-diderot.archives-ouvertes.fr\/hal-00154500\/document"},{"key":"S0960129518000075_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061361"},{"key":"S0960129518000075_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000989"},{"key":"S0960129518000075_ref3","volume-title":"Handbook of Categorical Algebra Volume 2. Categories and Structures","author":"Borceux","year":"2008"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000075","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,16]],"date-time":"2019-10-16T23:13:59Z","timestamp":1571267639000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000075\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,26]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,3]]}},"alternative-id":["S0960129518000075"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000075","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,4,26]]}}}