{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:33:57Z","timestamp":1750221237060,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,4,28]],"date-time":"2018-04-28T00:00:00Z","timestamp":1524873600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001381","name":"National Research Foundation of Singapore","doi-asserted-by":"crossref","award":["NRF2014NCR-NCR001-30"],"award-info":[{"award-number":["NRF2014NCR-NCR001-30"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"crossref","award":["12386"],"award-info":[{"award-number":["12386"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,4,30]]},"abstract":"<jats:p>\n            Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are \u201cabstract\u201d because they are independent of any particular concrete resource model. Their assertion languages, called\n            <jats:italic>Propositional Abstract Separation Logics<\/jats:italic>\n            (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in various ways. In particular, these logics contain the connectives * and \u2013*, denoting the composition and extension of resources, respectively.\n          <\/jats:p>\n          <jats:p>This added expressive power comes at a price, since the resulting logics are all undecidable. Given their wide applicability, even a semi-decision procedure for these logics is desirable. Although several PASLs and their relationships with BBI are discussed in the literature, the proof theory of, and automated reasoning for, these logics were open problems solved by the conference version of this article, which developed a modular proof theory for various PASLs using cut-free labelled sequent calculi. This paper non-trivially improves upon this previous work by giving a general framework of calculi on which any new axiom in the logic satisfying a certain form corresponds to an inference rule in our framework, and the completeness proof is generalised to consider such axioms.<\/jats:p>\n          <jats:p>Our base calculus handles Calcagno et al.\u2019s original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We then show that many important properties in separation logic, such as indivisible unit, disjointness, splittability, and cross-split, can be expressed in our general axiom form. Thus, our framework offers inference rules and completeness for these properties for free. Finally, we show how our calculi reduce to calculi with global label substitutions, enabling more efficient implementation.<\/jats:p>","DOI":"10.1145\/3197383","type":"journal-article","created":{"date-parts":[[2018,4,30]],"date-time":"2018-04-30T11:58:18Z","timestamp":1525089498000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Modular Labelled Sequent Calculi for Abstract Separation Logics"],"prefix":"10.1145","volume":"19","author":[{"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[{"name":"Griffith University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranald","family":"Clouston","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus N, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[{"name":"Australian National University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"Australian National University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,4,28]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Belnap Jr","author":"Anderson Alan Ross","year":"1976","unstructured":"Alan Ross Anderson and Nuel D . Belnap Jr . 1976 . Entailment, Vol . 1: The Logic of Relevance and Necessity. Princeton University Press , Princeton, NJ. Alan Ross Anderson and Nuel D. Belnap Jr. 1976. Entailment, Vol. 1: The Logic of Relevance and Necessity. Princeton University Press, Princeton, NJ."},{"key":"e_1_2_1_2_1","unstructured":"Franz Baader Diego Calvanese Deborah L. McGuinness Daniele Nardi and Peter F. Patel-Schneider (Eds.). 2003. The Description Logic Handbook: Theory Implementation and Applications. Cambridge University Press.   Franz Baader Diego Calvanese Deborah L. McGuinness Daniele Nardi and Peter F. Patel-Schneider (Eds.). 2003. The Description Logic Handbook: Theory Implementation and Applications. Cambridge University Press."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0372-3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"volume-title":"Static Analysis","author":"Boyland John","key":"e_1_2_1_7_1","unstructured":"John Boyland . 2003. Checking interference with fractional permissions . In Static Analysis . Springer , 55--72. John Boyland. 2003. Checking interference with fractional permissions. In Static Analysis. Springer, 55--72."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.012"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603091"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837621"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542667"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535844"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"Calcagno Cristiano","unstructured":"Cristiano Calcagno , Matthew Parkinson , and Viktor Vafeiadis . 2007. Modular safety checking for fine-grained concurrency . In Static Analysis . Lecture Notes in Computer Science , Vol. 4634 . Springer , 233--248. Cristiano Calcagno, Matthew Parkinson, and Viktor Vafeiadis. 2007. Modular safety checking for fine-grained concurrency. In Static Analysis. Lecture Notes in Computer Science, Vol. 4634. Springer, 233--248."},{"key":"e_1_2_1_16_1","volume-title":"O\u2019Hearn","author":"Calcagno Cristiano","year":"2001","unstructured":"Cristiano Calcagno , Hongseok Yang , and Peter W . O\u2019Hearn . 2001 . Computability and Complexity Results for a Spatial Assertion Language for Data Structures. Springer , Berlin, Germany, 108--119. Cristiano Calcagno, Hongseok Yang, and Peter W. O\u2019Hearn. 2001. Computability and Complexity Results for a Spatial Assertion Language for Data Structures. Springer, Berlin, Germany, 108--119."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529402"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2835490"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-016-9713-1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926416"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_1_23_1","volume-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting Melvin","unstructured":"Melvin Fitting . 1996. First-Order Logic and Automated Theorem Proving ( 2 nd ed.). Springer-Verlag New York , Secaucus, NJ . Melvin Fitting. 1996. First-Order Logic and Automated Theorem Proving (2nd ed.). Springer-Verlag New York, Secaucus, NJ.","edition":"2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_33"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn066"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.021"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2009.8.4.a3"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535864"},{"key":"e_1_2_1_30_1","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction (CADE)","author":"H\u00f3u Zh\u00e9","unstructured":"Zh\u00e9 H\u00f3u , Rajeev Gor\u00e9 , and Alwen Tiu . 2015. Automated theorem proving for assertions in separation logic with all connectives . In Automated Deduction (CADE) . Lecture Notes in Computer Science , Vol. 9195 . Springer , 501--516. Zh\u00e9 H\u00f3u, Rajeev Gor\u00e9, and Alwen Tiu. 2015. Automated theorem proving for assertions in separation logic with all connectives. In Automated Deduction (CADE). Lecture Notes in Computer Science, Vol. 9195. Springer, 501--516."},{"key":"e_1_2_1_31_1","volume-title":"Separata: Isabelle tactics for separation algebra. Archive of Formal Proofs. Retrieved","author":"H\u00f3u Zh\u00e9","year":"2016","unstructured":"Zh\u00e9 H\u00f3u , David Sanan , Alwen Tiu , Rajeev Gor\u00e9 , and Ranald Clouston . 2016 . Separata: Isabelle tactics for separation algebra. Archive of Formal Proofs. Retrieved April 5, 2018, from http:\/\/isa-afp.org\/entries\/Separata.shtml. Zh\u00e9 H\u00f3u, David Sanan, Alwen Tiu, Rajeev Gor\u00e9, and Ranald Clouston. 2016. Separata: Isabelle tactics for separation algebra. Archive of Formal Proofs. Retrieved April 5, 2018, from http:\/\/isa-afp.org\/entries\/Separata.shtml."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_19"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_23"},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)","author":"H\u00f3u Zh\u00e9","unstructured":"Zh\u00e9 H\u00f3u , Alwen Tiu , and Rajeev Gor\u00e9 . 2013. A labelled sequent calculus for BBI: Proof theory and proof search . In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) . Lecture Notes in Computer Science , Vol. 8123 . Springer , 172--187. Zh\u00e9 H\u00f3u, Alwen Tiu, and Rajeev Gor\u00e9. 2013. A labelled sequent calculus for BBI: Proof theory and proof search. In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). Lecture Notes in Computer Science, Vol. 8123. Springer, 172--187."},{"key":"e_1_2_1_35_1","first-page":"1","article-title":"A labelled sequent calculus for BBI: Proof theory and proof search","volume":"1","author":"H\u00f3u Zh\u00e9","year":"2015","unstructured":"Zh\u00e9 H\u00f3u , Alwen Tiu , and Rajeev Gor\u00e9 . 2015 . A labelled sequent calculus for BBI: Proof theory and proof search . J. Logic Comput. 1 , 1 -- 64 . Zh\u00e9 H\u00f3u, Alwen Tiu, and Rajeev Gor\u00e9. 2015. A labelled sequent calculus for BBI: Proof theory and proof search. J. Logic Comput. 1, 1--64.","journal-title":"J. Logic Comput."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429105"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_1_40_1","volume-title":"Separation algebra. Archive of Formal Proofs. Retrieved","author":"Klein Gerwin","year":"2018","unstructured":"Gerwin Klein , Rafal Kolanski , and Andrew Boyton . 2012. Separation algebra. Archive of Formal Proofs. Retrieved April 5, 2018 , from http:\/\/isa-afp.org\/entries\/Separation_Algebra.shtml. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. 2012. Separation algebra. Archive of Formal Proofs. Retrieved April 5, 2018, from http:\/\/isa-afp.org\/entries\/Separation_Algebra.shtml."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181195.1181213"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu031"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007567"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.18"},{"key":"e_1_2_1_45_1","series-title":"Lecture Notes in Computer Science","volume-title":"Theoretical Computer Science","author":"Larchey-Wendling Dominique","unstructured":"Dominique Larchey-Wendling and Didier Galmiche . 2014. Looking at separation algebras with Boolean BI-eyes . In Theoretical Computer Science . Lecture Notes in Computer Science , Vol. 8705 . Springer , 326--340. Dominique Larchey-Wendling and Didier Galmiche. 2014. Looking at separation algebras with Boolean BI-eyes. In Theoretical Computer Science. Lecture Notes in Computer Science, Vol. 8705. Springer, 326--340."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535871"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"volume-title":"Structural Proof Theory","author":"Negri Sara","key":"e_1_2_1_49_1","unstructured":"Sara Negri and Jan von Plato . 2001. Structural Proof Theory . Cambridge University Press . Sara Negri and Jan von Plato. 2001. Structural Proof Theory. Cambridge University Press."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429095"},{"volume-title":"Verified Software: Theories, Tools, Experiments (VSTTE).","author":"Parkinson Matthew","key":"e_1_2_1_53_1","unstructured":"Matthew Parkinson . 2010. The next 700 separation logics . In Verified Software: Theories, Tools, Experiments (VSTTE). Vol. 6217 . Springer , 169--182. Matthew Parkinson. 2010. The next 700 separation logics. In Verified Software: Theories, Tools, Experiments (VSTTE). Vol. 6217. Springer, 169--182."},{"volume-title":"A Decision Procedure for Separation Logic in SMT","author":"Reynolds Andrew","key":"e_1_2_1_54_1","unstructured":"Andrew Reynolds , Radu Iosif , Cristina Serban , and Tim King . 2016. A Decision Procedure for Separation Logic in SMT . Springer International Publishing , Cham , 244--261. Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. 2016. A Decision Procedure for Separation Logic in SMT. Springer International Publishing, Cham, 244--261."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_56_1","unstructured":"Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier Science Publishers B.V. Amsterdam Netherlands.   Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier Science Publishers B.V. Amsterdam Netherlands."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_2_1_58_1","first-page":"614","article-title":"Lightweight support for magic wands in an automatic verifier","volume":"37","author":"Schwerhoff Malte","year":"2015","unstructured":"Malte Schwerhoff and Alexander J. Summers . 2015 . Lightweight support for magic wands in an automatic verifier . Leibniz Int. Proc. Informat. 37 , 614 -- 638 . Malte Schwerhoff and Alexander J. Summers. 2015. Lightweight support for magic wands in an automatic verifier. Leibniz Int. Proc. Informat. 37, 614--638.","journal-title":"Leibniz Int. Proc. Informat."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632376"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_32"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509532"},{"key":"e_1_2_1_64_1","series-title":"Lecture Notes in Computer Science","volume-title":"Concurrency Theory (CONCUR)","author":"Vafeiadis Viktor","unstructured":"Viktor Vafeiadis and Matthew Parkinson . 2007. A marriage of rely\/guarantee and separation logic . In Concurrency Theory (CONCUR) . Lecture Notes in Computer Science , Vol. 4703 . Springer , 256--271. Viktor Vafeiadis and Matthew Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In Concurrency Theory (CONCUR). Lecture Notes in Computer Science, Vol. 4703. Springer, 256--271."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_15"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3197383","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3197383","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:18Z","timestamp":1750212438000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3197383"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,28]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4,30]]}},"alternative-id":["10.1145\/3197383"],"URL":"https:\/\/doi.org\/10.1145\/3197383","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,4,28]]},"assertion":[{"value":"2017-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-04-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}