{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T20:02:25Z","timestamp":1694635345994},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,6,1]],"date-time":"2009-06-01T00:00:00Z","timestamp":1243814400000},"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":[[2009,6]]},"abstract":"<jats:p>The logic of Bunched Implications, through both its intuitionistic version (<jats:monospace>BI<\/jats:monospace>) and one of its classical versions, called Boolean<jats:monospace>BI<\/jats:monospace>(<jats:monospace>BBI<\/jats:monospace>), serves as a logical basis to spatial or separation logic frameworks. In<jats:monospace>BI<\/jats:monospace>, the logical implication is interpreted intuitionistically whereas it is generally interpreted classically in spatial or separation logics, as in<jats:monospace>BBI<\/jats:monospace>. In this paper, we aim to give some new insights into the semantic relations between<jats:monospace>BI<\/jats:monospace>and<jats:monospace>BBI<\/jats:monospace>. Then we propose a sound and complete syntactic constraints based framework for the Kripke semantics of both<jats:monospace>BI<\/jats:monospace>and<jats:monospace>BBI<\/jats:monospace>, a sound labelled tableau proof system for<jats:monospace>BBI<\/jats:monospace>, and a representation theorem relating the syntactic models of<jats:monospace>BI<\/jats:monospace>to those of<jats:monospace>BBI<\/jats:monospace>. Finally, we deduce as our main, and unexpected, result, a sound and faithful embedding of<jats:monospace>BI<\/jats:monospace>into<jats:monospace>BBI<\/jats:monospace>.<\/jats:p>","DOI":"10.1017\/s0960129509007567","type":"journal-article","created":{"date-parts":[[2009,4,16]],"date-time":"2009-04-16T08:51:22Z","timestamp":1239871882000},"page":"435-500","source":"Crossref","is-referenced-by-count":20,"title":["Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding"],"prefix":"10.1017","volume":"19","author":[{"given":"DOMINIQUE","family":"LARCHEY-WENDLING","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DIDIER","family":"GALMICHE","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,6,1]]},"reference":[{"key":"S0960129509007567_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.04.021"},{"key":"S0960129509007567_ref12","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/360204.375719","volume-title":"Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Ishtiaq","year":"2001"},{"key":"S0960129509007567_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005404"},{"key":"S0960129509007567_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_24"},{"key":"S0960129509007567_ref6","first-page":"365","volume-title":"Proceedings of the 27th ACM SIGPLAN-SIGACT Principles of Programming Languages conference","author":"Cardelli","year":"2000"},{"key":"S0960129509007567_ref10","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.707"},{"key":"S0960129509007567_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"S0960129509007567_ref17","first-page":"183","volume-title":"Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science","author":"Pym","year":"1999"},{"key":"S0960129509007567_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"S0960129509007567_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"S0960129509007567_ref5","first-page":"123","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Calcagno","year":"2007"},{"key":"S0960129509007567_ref9","first-page":"358","article-title":"Expressivity properties of Boolean BI through Relational Models. In: Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science","volume":"4337","author":"Galmiche","year":"2006","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129509007567_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.020"},{"key":"S0960129509007567_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_18"},{"key":"S0960129509007567_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61208-4_16"},{"key":"S0960129509007567_ref14","unstructured":"M\u00e9ry D. (2004) Preuves et S\u00e9mantiques dans des Logiques de Ressources, Ph.D. thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy I, France. (Available at http:\/\/www.loria.fr\/~dmery\/these.pdf.)"},{"key":"S0960129509007567_ref18","article-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","volume":"26","author":"Pym","year":"2002","journal-title":"Applied Logic Series"},{"key":"S0960129509007567_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0018-z"},{"key":"S0960129509007567_ref1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm019"},{"key":"S0960129509007567_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.020"},{"key":"S0960129509007567_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90006-9"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129509007567","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,4]],"date-time":"2021-10-04T05:37:01Z","timestamp":1633325821000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129509007567\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["S0960129509007567"],"URL":"https:\/\/doi.org\/10.1017\/s0960129509007567","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6]]}}}