{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T10:10:10Z","timestamp":1746353410559,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642387081"},{"type":"electronic","value":"9783642387098"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44602-7_25","type":"book-chapter","created":{"date-parts":[[2014,8,23]],"date-time":"2014-08-23T01:18:40Z","timestamp":1408756720000},"page":"326-340","source":"Crossref","is-referenced-by-count":2,"title":["Looking at Separation Algebras with Boolean BI-eyes"],"prefix":"10.1007","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":"297","reference":[{"issue":"6","key":"25_CR1","doi-asserted-by":"publisher","first-page":"1223","DOI":"10.1007\/s11225-012-9449-0","volume":"100","author":"J. Brotherston","year":"2012","unstructured":"Brotherston, J.: Bunched Logics Displayed. Studia Logica\u00a0100(6), 1223\u20131254 (2012)","journal-title":"Studia Logica"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of Propositional Separation Logic and Its Neighbours. In: LICS, pp. 130\u2013139. IEEE Computer Society (2010)","DOI":"10.1109\/LICS.2010.24"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of Propositional Separation Logic and its Neighbours. Journal of the ACM\u00a061(2) (2014)","DOI":"10.1145\/2542667"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J.: Parametric Completeness for Separation Theories. In: POPL, pp. 453\u2013464. ACM (2014)","DOI":"10.1145\/2535838.2535844"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local Action and Abstract Separation Logic. In: LICS, pp. 366\u2013378. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL, pp. 287\u2013300. ACM (2013)","DOI":"10.1145\/2480359.2429104"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","volume-title":"Programming Languages and Systems","author":"R. Dockins","year":"2009","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A Fresh Look at Separation Algebras and Share Accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 161\u2013177. Springer, Heidelberg (2009)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/11944836_33","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"D. Galmiche","year":"2006","unstructured":"Galmiche, D., Larchey-Wendling, D.: Expressivity properties of Boolean BI through Relational Models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 357\u2013368. Springer, Heidelberg (2006)"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"H\u00f3u, Z., Clouston, R., Gor\u00e9, R., Tiu, A.: Proof search for propositional abstract separation logics via labelled sequents. In: POPL, pp. 465\u2013476. ACM (2014)","DOI":"10.1145\/2535838.2535864"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-40537-2_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Z. H\u00f3u","year":"2013","unstructured":"H\u00f3u, Z., Tiu, A., Gor\u00e9, R.: A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol.\u00a08123, pp. 172\u2013187. Springer, Heidelberg (2013)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: POPL, London, UK, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D.: The formal strong completeness of partial monoidal Boolean BI. J. Logic. Comput. (2014), http:\/\/dx.doi.org\/10.1093\/logcom\/exu031 , doi:10.1093\/logcom\/exu031","DOI":"10.1093\/logcom\/exu031"},{"issue":"3","key":"25_CR13","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1017\/S0960129509007567","volume":"19","author":"D. Larchey-Wendling","year":"2009","unstructured":"Larchey-Wendling, D., Galmiche, D.: Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding. Mathematical Structures in Computer Science\u00a019(3), 435\u2013500 (2009)","journal-title":"Mathematical Structures in Computer Science"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: The Undecidability of Boolean BI through Phase Semantics. In: LICS, pp. 140\u2013149. IEEE Computer Society (2010)","DOI":"10.1109\/LICS.2010.18"},{"issue":"1","key":"25_CR15","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2422085.2422091","volume":"14","author":"D. Larchey-Wendling","year":"2013","unstructured":"Larchey-Wendling, D., Galmiche, D.: Nondeterministic Phase Semantics and the Undecidability of Boolean BI. ACM ToCL\u00a014(1), 6 (2013)","journal-title":"ACM ToCL"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL, pp. 219\u2013232. ACM (2013)","DOI":"10.1145\/2480359.2429095"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol.\u00a026. Kluwer Academic Publishers (2002)","DOI":"10.1007\/978-94-017-0091-7"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Advanced Information Systems Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44602-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T09:40:53Z","timestamp":1746351653000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44602-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642387081","9783642387098"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44602-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}