{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T06:22:12Z","timestamp":1746253332437},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540499947"},{"type":"electronic","value":"9783540499954"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11944836_33","type":"book-chapter","created":{"date-parts":[[2006,11,28]],"date-time":"2006-11-28T04:48:02Z","timestamp":1164689282000},"page":"357-368","source":"Crossref","is-referenced-by-count":23,"title":["Expressivity Properties of Boolean BI Through Relational Models"],"prefix":"10.1007","author":[{"given":"Didier","family":"Galmiche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Larchey-Wendling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. Cambridge University Press, New York (2001)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45694-5_15","volume-title":"CONCUR 2002 - Concurrency Theory","author":"L. Caires","year":"2002","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency (Part II). In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 209\u2013225. Springer, Heidelberg (2002)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-28644-8_16","volume-title":"CONCUR 2004 - Concurrency Theory","author":"L. Caires","year":"2004","unstructured":"Caires, L., Lozes, \u00c9.: Elimination of quantifiers and undecidability in spatial logics for concurrency. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 240\u2013257. Springer, Heidelberg (2004)"},{"key":"33_CR4","volume-title":"Cambridge Mathematical Textbooks","author":"B. Davey","year":"1990","unstructured":"Davey, B., Priestley, H.: Introduction to Lattices and Order. In: Cambridge Mathematical Textbooks. Cambridge University Press, Cambridge (1990)"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-30538-5_18","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"A. Dawar","year":"2004","unstructured":"Dawar, A., Gardner, P., Ghelli, G.: Adjunct elimination through games in static ambient logic(Extended abstract). In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 211\u2013223. Springer, Heidelberg (2004)"},{"issue":"5","key":"33_CR6","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1093\/logcom\/13.5.707","volume":"13","author":"D. Galmiche","year":"2003","unstructured":"Galmiche, D., M\u00e9ry, D.: Semantic labelled tableaux for propositional BI without bottom. Journal of Logic and Computation\u00a013(5), 707\u2013753 (2003)","journal-title":"Journal of Logic and Computation"},{"key":"33_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11591191_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Galmiche","year":"2005","unstructured":"Galmiche, D., M\u00e9ry, D.: Characterizing provability in BI\u2019s pointer logic through resource graphs. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 459\u2013473. Springer, Heidelberg (2005)"},{"issue":"6","key":"33_CR8","doi-asserted-by":"publisher","first-page":"1033","DOI":"10.1017\/S0960129505004858","volume":"15","author":"D. Galmiche","year":"2005","unstructured":"Galmiche, D., M\u00e9ry, D., Pym, D.: The semantics of BI and Resource Tableaux. Math. Struct. in Comp. Science\u00a015(6), 1033\u20131088 (2005)","journal-title":"Math. Struct. in Comp. Science"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: 28th ACM Symposium on Principles of Programming Languages, London, pp. 14\u201326 (2001)","DOI":"10.1145\/360204.375719"},{"key":"33_CR10","series-title":"International series in computer science","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. International series in computer science. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"33_CR12","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"D. Pym","year":"2002","unstructured":"Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol.\u00a026. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"33_CR13","unstructured":"Pym, D., Tofts, C.: A calculus and logic of resources and processes. Technical Report HPL-2004-170, HP Labs (2004)"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science, Copenhagen, July 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"33_CR15","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R.: Intuitionistic Propositional Logic is Polynomial-Space Complete. Theoretical Computer Science\u00a09, 67\u201372 (1979)","journal-title":"Theoretical Computer Science"},{"key":"33_CR16","unstructured":"Yang, H.: Ternary-relation Models of Boolean BI: Soundness and Completeness (unpublished note) (2004)"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11944836_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:17:49Z","timestamp":1619507869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11944836_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540499947","9783540499954"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11944836_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}