{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:39:43Z","timestamp":1757309983243,"version":"3.40.4"},"reference-count":30,"publisher":"Oxford University Press (OUP)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1093\/logcom\/exu031","type":"journal-article","created":{"date-parts":[[2014,6,3]],"date-time":"2014-06-03T02:29:42Z","timestamp":1401762582000},"page":"605-640","source":"Crossref","is-referenced-by-count":13,"title":["The formal strong completeness of partial monoidal Boolean BI"],"prefix":"10.1093","volume":"26","author":[{"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2014,6,2]]},"reference":[{"key":"2016032907475299000_26.2.605.1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.012"},{"key":"2016032907475299000_26.2.605.2","doi-asserted-by":"crossref","unstructured":"Brotherston J. Calcagno C. Classical BI: a logic for reasoning about dualising resources. In: Shao Z. Pierce B. C. , editors. POPL. ACM; 2009. p. 328-339.","DOI":"10.1145\/1594834.1480923"},{"key":"2016032907475299000_26.2.605.3","doi-asserted-by":"crossref","unstructured":"Brotherston J. Calcagno C. Classical BI: its semantics and proof theory. Logical Methods in Computer Science 2010;6.","DOI":"10.2168\/LMCS-6(3:3)2010"},{"key":"2016032907475299000_26.2.605.4","doi-asserted-by":"crossref","unstructured":"Brotherston J. Kanovich M. I. 25th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society; 2010. Undecidability of propositional separation logic and its neighbours; p. 130-139.","DOI":"10.1109\/LICS.2010.24"},{"key":"2016032907475299000_26.2.605.5","doi-asserted-by":"crossref","unstructured":"Brotherston J. Villard J. POPL. ACM; 2014. Parametric completeness for separation theories; p. 453-464.","DOI":"10.1145\/2535838.2535844"},{"key":"2016032907475299000_26.2.605.6","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005404"},{"key":"2016032907475299000_26.2.605.7","doi-asserted-by":"crossref","unstructured":"Calcagno C. O'Hearn P. W. Yang H. 22nd IEEE Symposium on Logic in Computer Science. IEEE Computer Society; 2007. Local action and abstract separation logic; p. 366-378.","DOI":"10.1109\/LICS.2007.30"},{"key":"2016032907475299000_26.2.605.8","doi-asserted-by":"crossref","unstructured":"Chicli L. Pottier L. Simpson C. Mathematical quotients and quotient types in Coq. In: Geuvers H. Wiedijk F. , editors. Types for Proofs and Programs, vol. 2646 of Lecture Notes in Computer Science . Springer Berlin Heidelberg; 2003. p. 95-107.","DOI":"10.1007\/3-540-39185-1_6"},{"key":"2016032907475299000_26.2.605.9","doi-asserted-by":"crossref","unstructured":"Coquand T. Huet G. P. Constructions: a higher order proof system for mechanizing mathematics. In: Buchberger B. , editor. European Conference on Computer Algebra (1), vol. 203 of Lecture Notes in Computer Science . Springer; 1985. p. 151-184.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"2016032907475299000_26.2.605.10","doi-asserted-by":"crossref","unstructured":"Courtault J.-R. Galmiche D. A modal BI logic for dynamic resource properties. In: Artemov S. Nerode A. , editors. Symposium on Logical Foundations of Computer Science, vol. 7734 of Lecture Notes in Computer Science . Springer-Verlag Berlin Heidelberg; 2013. p. 134-148.","DOI":"10.1007\/978-3-642-35722-0_10"},{"key":"2016032907475299000_26.2.605.11","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-005-0321-z"},{"key":"2016032907475299000_26.2.605.12","doi-asserted-by":"crossref","unstructured":"Fitting M. First-order Logic and Automated Theorem Proving. Springer-Verlag New York, Inc.; 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"2016032907475299000_26.2.605.13","doi-asserted-by":"crossref","unstructured":"Galmiche D. Larchey-Wendling D. Expressivity properties of Boolean BI through Relational models. In: Arun-Kumar S. Garg N. , editors. 26th Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 4337 of Lecture Notes in Computer Science . Springer; 2006. p. 358-369.","DOI":"10.1007\/11944836_33"},{"key":"2016032907475299000_26.2.605.14","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"2016032907475299000_26.2.605.15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2016032907475299000_26.2.605.16","first-page":"7","article-title":"Form and content in quantification theory","volume":"8","author":"Hintikka","year":"1955","journal-title":"Acta Philosophica Fennica"},{"key":"2016032907475299000_26.2.605.17","doi-asserted-by":"crossref","unstructured":"H\u00f3u Z. Clouston R. Gor\u00e9 R. Tiu A. POPL. ACM; 2014. Proof search for propositional abstract separation logics via labelled sequents; p. 465-476.","DOI":"10.1145\/2535838.2535864"},{"key":"2016032907475299000_26.2.605.18","doi-asserted-by":"crossref","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. , editors. TABLEAUX, vol. 8123 of Lecture Notes in Computer Science . Springer; 2013. p. 172-187.","DOI":"10.1007\/978-3-642-40537-2_16"},{"key":"2016032907475299000_26.2.605.19","doi-asserted-by":"crossref","unstructured":"Ishtiaq S. S. O'Hearn P. W. 28th ACM Symposium on Principles of Programming Languages, POPL 2001 . London, UK; 2001. BI as an assertion language for mutable data structures; p. 14-26.","DOI":"10.1145\/373243.375719"},{"key":"2016032907475299000_26.2.605.20","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.022"},{"key":"2016032907475299000_26.2.605.21","unstructured":"D. Larchey-Wendling and D. Galmiche. Looking at Separation Algebras with Boolean BI-eyes. Available athttp:\/\/www.loria.fr\/\u223clarchey\/papers\/tcs_larcheyw_galmiche.pdf."},{"key":"2016032907475299000_26.2.605.22","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007567"},{"key":"2016032907475299000_26.2.605.23","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling D. Galmiche D. 25th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society; 2010. The Undecidability of Boolean BI through Phase Semantics; p. 140-149.","DOI":"10.1109\/LICS.2010.18"},{"key":"2016032907475299000_26.2.605.24","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling D. Galmiche D. Non-deterministic phase semantics and the undecidability of Boolean BI. ACM Transactions on Computational Logic 2013;14.","DOI":"10.1145\/2422085.2422091"},{"key":"2016032907475299000_26.2.605.25","unstructured":"M\u00e9ry D. PhD Thesis. Universit\u00e9 Henri Poincar\u00e9, Nancy I; 2004. Preuves et S\u00e9mantiques dans des Logiques de Ressources. Available athttp:\/\/www.loria.fr\/~dmery\/these.pdf."},{"key":"2016032907475299000_26.2.605.26","doi-asserted-by":"crossref","unstructured":"O'Hearn P. W. Reynolds J. C. Yang H. 15th Int. Workshop on Computer Science Logic, vol. 2142 of Lecture Notes in Computer Science . Paris, France; 2001. Local reasoning about programs that alter data structures; p. 1-19.","DOI":"10.1007\/3-540-44802-0_1"},{"key":"2016032907475299000_26.2.605.27","doi-asserted-by":"crossref","unstructured":"Park J. Seo J. Park S. A theorem prover for Boolean BI. In: Giacobazzi R. Cousot R. , editors. POPL. ACM; 2013. p. 219-232.","DOI":"10.1145\/2480359.2429095"},{"key":"2016032907475299000_26.2.605.28","doi-asserted-by":"crossref","unstructured":"Pfenning F. Paulin-Mohring C. Inductively defined types in the calculus of constructions. In: Main M. G. Melton A. Mislove M. W. Schmidt D. A. , editors. Mathematical Foundations of Programming Semantics, 5th International Conference, vol. 442 of Lecture Notes in Computer Science . Springer; 1989. p. 209-228.","DOI":"10.1007\/BFb0040259"},{"key":"2016032907475299000_26.2.605.29","doi-asserted-by":"crossref","unstructured":"Pym D. J. 14th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society; 1999. On bunched predicate logic; p. 183-192.","DOI":"10.1109\/LICS.1999.782614"},{"key":"2016032907475299000_26.2.605.30","doi-asserted-by":"crossref","unstructured":"Pym D. J. The Semantics and Proof Theory of the Logic of Bunched Implications, vol. 26 of Applied Logic Series . Kluwer Academic Publishers; 2002.","DOI":"10.1007\/978-94-017-0091-7"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/26\/2\/605\/7950216\/exu031.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T06:16:16Z","timestamp":1746252976000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exu031"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,2]]},"references-count":30,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,3,29]]},"published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1093\/logcom\/exu031"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exu031","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published":{"date-parts":[[2014,6,2]]}}}