{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T18:54:38Z","timestamp":1648580078868},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"10","license":[{"start":{"date-parts":[[2019,9,16]],"date-time":"2019-09-16T00:00:00Z","timestamp":1568592000000},"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,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we continue with the algebraic study of Krivine\u2019s realizability, completing and generalizing some of the authors\u2019 previous constructions by introducing two categories with objects the abstract Krivine structures and the implicative algebras, respectively. These categories are related by an adjunction whose existence clarifies many aspects of the theory previously established. We also revisit, reinterpret, and generalize in categorical terms, some of the results of our previous work such as: the bullet construction, the equivalence of Krivine\u2019s, Streicher\u2019s, and bullet triposes and also the fact that these triposes can be obtained \u2013 up to equivalence \u2013 from implicative algebras or implicative ordered combinatory algebras.<\/jats:p>","DOI":"10.1017\/s0960129519000100","type":"journal-article","created":{"date-parts":[[2019,9,16]],"date-time":"2019-09-16T13:42:31Z","timestamp":1568641351000},"page":"1575-1606","source":"Crossref","is-referenced-by-count":0,"title":["The category of implicative algebras and realizability"],"prefix":"10.1017","volume":"29","author":[{"given":"Walter","family":"Ferrer Santos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Octavio","family":"Malherbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,9,16]]},"reference":[{"key":"S0960129519000100_ref25","first-page":"571","article-title":"Classical and relative realizability","volume":"31","author":"van Oosten","year":"2016","journal-title":"Theory and Applications of Categories"},{"key":"S0960129519000100_ref24","volume-title":"Realizability, An Introduction to its Categorical Side","author":"van Oosten","year":"2008"},{"key":"S0960129519000100_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"S0960129519000100_ref20","unstructured":"Miquel, A. (February 2018). Implicative algebras: a new foundation for forcing and realizability. https:\/\/arxiv.org\/abs\/1802.00528."},{"key":"S0960129519000100_ref19","unstructured":"Miquel, A. (2016). Implicative algebras: a new foundation for forcing and realizability. In: Workshop. Realizability in Uruguay, Piriapolis. \/\/www.p\u00e9drot.fr\/montevideo2016\/miquel-slides.pdf"},{"key":"S0960129519000100_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000989"},{"key":"S0960129519000100_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129519000100_ref16","unstructured":"Krivine, J.-L. (2009). Realizability in classical logic in interactive models of computation and program behaviour. Panoramas et synth\u00e8ses 27, SMF."},{"key":"S0960129519000100_ref15","unstructured":"Krivine, J.-L. (2008). Structures de r\u00e9alisabilit\u00e9, RAM et ultrafiltre sur ,. http:\/\/www.pps.jussieu.fr\/krivine\/Ultrafiltre.pdf."},{"key":"S0960129519000100_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00776-4"},{"key":"S0960129519000100_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000057"},{"key":"S0960129519000100_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S0960129519000100_ref21","unstructured":"Miquey, E. (2017). R\u00e9alisabilit\u00e9 classique et effets de bords. http:\/\/www.theses.fr\/s180391."},{"key":"S0960129519000100_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004102006424"},{"key":"S0960129519000100_ref18","unstructured":"Miquel, A. (2014). Implicative algebras for non commutative forcing. In: Workshop. Mathematical Structures in Computation, Lyon. \/\/smc2014.univ-lyon1.fr\/lib\/exe\/fetch.php?media=miquel.pdf"},{"key":"S0960129519000100_ref5","first-page":"1","volume-title":"Mathematical Structures in Computer Science","author":"Ferrer Santos","year":"2015"},{"key":"S0960129519000100_ref1","volume-title":"Lattice Theory","author":"Birkhoff","year":"1995"},{"key":"S0960129519000100_ref3","volume-title":"Handbook of Categorical Algebra Volume 2. Categories and Structures (Encyclopedia of Mathematics and its Applications, 51).","author":"Borceux","year":"2008"},{"key":"S0960129519000100_ref2","volume-title":"Handbook of Categorical Algebra Volume 1. Basic Category Theory (Encyclopedia of Mathematics and its Applications, 50)","author":"Borceux","year":"2008"},{"key":"S0960129519000100_ref4","unstructured":"Ferrer Santos, W. , Guillermo, M. and Malherbe, O. (2013). A Report on Realizability, https:\/\/arxiv.org\/abs\/1309.0706v3 [math.LO], 1\u201325."},{"key":"S0960129519000100_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000075"},{"key":"S0960129519000100_ref7","unstructured":"Gr\u00e4tzer, G. (1978). General Lattice Theory, Mathematische Reihe Lehrb\u00fccher und Monographien aus dem Gebiete der Exakten Wissenschaften 52, Birkh\u00e4user, Basel."},{"key":"S0960129519000100_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004106009352"},{"key":"S0960129519000100_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004107000400"},{"key":"S0960129519000100_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70129-6"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129519000100","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,28]],"date-time":"2019-11-28T10:23:06Z","timestamp":1574936586000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129519000100\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,16]]},"references-count":25,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["S0960129519000100"],"URL":"https:\/\/doi.org\/10.1017\/s0960129519000100","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,16]]}}}