{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:34:04Z","timestamp":1757313244924,"version":"3.41.0"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893655"},{"type":"electronic","value":"9783319893662"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89366-2_24","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T23:52:34Z","timestamp":1523663554000},"page":"441-458","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Modular Tableaux Calculi for Separation Theories"],"prefix":"10.1007","author":[{"given":"Simon","family":"Docherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pym","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.tcs.2015.11.035","volume":"614","author":"G Anderson","year":"2016","unstructured":"Anderson, G., Pym, D.: A calculus and logic of bunched resources and processes. Theoret. Comput. Sci. 614, 63\u201396 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Program Logics for Certified Compilers. CUP (2014)","DOI":"10.1017\/CBO9781107256552"},{"issue":"17","key":"24_CR3","first-page":"1","volume":"2","author":"R Atkey","year":"2011","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Log. Methods Comput. Sci. 2(17), 1\u201333 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/11591191_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Bezem","year":"2005","unstructured":"Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 246\u2013260. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_18"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115\u2013137. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_6"},{"issue":"1","key":"24_CR6","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/1047659.1040327","volume":"40","author":"Richard Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of POPL 2005, pp. 259\u2013270. ACM (2005)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"key":"24_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0002-4","volume-title":"Hybrid Logic and Its Proof-Theory. Applied Logic Series","author":"T Bra\u00fcner","year":"2011","unstructured":"Bra\u00fcner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series, vol. 37. Springer, Dordrecht (2011)"},{"issue":"6","key":"24_CR9","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. Stud. Logica. 100(6), 1223\u20131254 (2012)","journal-title":"Stud. Logica."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: Proceedings of POPL 2014, pp. 453\u2013464. ACM (2014)","DOI":"10.1145\/2535838.2535844"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Buisse, A., Birkedal, L., St\u00f8vring, K.: A step-indexed Kripke model of separation logic for storable locks. In: Proceedings of MFPS XXVII, ENTCS, vol. 276, pp. 121\u2013143 (2011)","DOI":"10.1016\/j.entcs.2011.09.018"},{"issue":"6","key":"24_CR12","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011). https:\/\/doi.org\/10.1145\/2049697.2049700","journal-title":"J. ACM"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. In: Proceedings of LICS 2007, pp. 366\u2013378. IEEE (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-71237-6_10","volume-title":"Programming Languages and Systems","author":"Q Cao","year":"2017","unstructured":"Cao, Q., Cuellar, S., Appel, A.W.: Bringing order to the separation logic jungle. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 190\u2013211. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_10"},{"key":"24_CR15","volume-title":"Theories, Sites, Toposes: Relating and Studying Mathematical Theories Through Topos-Theoretic \u2018Bridges\u2019","author":"O Caramello","year":"2017","unstructured":"Caramello, O.: Theories, Sites, Toposes: Relating and Studying Mathematical Theories Through Topos-Theoretic \u2018Bridges\u2019. OUP, Oxford (2017)"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of SOSP 2015, pp. 18\u201337. ACM (2015)","DOI":"10.1145\/2815400.2815402"},{"issue":"4","key":"24_CR17","doi-asserted-by":"publisher","first-page":"953","DOI":"10.1093\/logcom\/exu002","volume":"24","author":"M Collinson","year":"2014","unstructured":"Collinson, M., McDonald, K., Pym, D.: A substructural logic for layered graphs. J. Log. Comput. 24(4), 953\u2013988 (2014)","journal-title":"J. Log. Comput."},{"issue":"1","key":"24_CR18","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1093\/logcom\/exv020","volume":"27","author":"M Collinson","year":"2017","unstructured":"Collinson, M., McDonald, K., Pym, D.: Layered graph logic as an assertion language for access control policy models. J. Log. Comput. 27(1), 41\u201380 (2017)","journal-title":"J. Log. Comput."},{"key":"24_CR19","doi-asserted-by":"publisher","first-page":"959","DOI":"10.1017\/S0960129509990077","volume":"19","author":"M Collinson","year":"2009","unstructured":"Collinson, M., Pym, D.: Algebra and logic for resource-based systems modelling. Math. Struct. Comput. Sci. 19, 959\u20131027 (2009)","journal-title":"Math. Struct. Comput. Sci."},{"key":"24_CR20","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1016\/j.tcs.2016.04.040","volume":"637","author":"J-R Courtault","year":"2016","unstructured":"Courtault, J.-R., Galmiche, D., Pym, D.: A logic of separating modalities. Theoret. Comput. Sci. 637, 30\u201358 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: Proceedings of POPL 2013, pp. 287\u2013300 (2013)","DOI":"10.1145\/2480359.2429104"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-319-40229-1_32","volume-title":"Automated Reasoning","author":"S Docherty","year":"2016","unstructured":"Docherty, S., Pym, D.: Intuitionistic layered graph logic. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 469\u2013486. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_32"},{"key":"24_CR23","unstructured":"Docherty, S., Pym, D.: Stone-Type Dualities for Separation Logics (Submitted)"},{"key":"24_CR24","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. 5904, pp. 161\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13"},{"issue":"2","key":"24_CR25","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/bsl.2015.7","volume":"21","author":"R Dyckhoff","year":"2015","unstructured":"Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symb. Log. 21(2), 123\u2013163 (2015)","journal-title":"Bull. Symb. Log."},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-662-54069-5_9","volume-title":"Logic and Its Applications","author":"D Galmiche","year":"2017","unstructured":"Galmiche, D., Kimmel, P., Pym, D.: A substructural epistemic resource logic. In: Ghosh, S., Prasad, S. (eds.) ICLA 2017. LNCS, vol. 10119, pp. 106\u2013122. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54069-5_9"},{"issue":"1","key":"24_CR27","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1093\/logcom\/exn066","volume":"20","author":"D Galmiche","year":"2007","unstructured":"Galmiche, D., M\u00e9ry, D.: Tableaux and resource graphs for separation logic. J. Log. Comput. 20(1), 189\u2013231 (2007)","journal-title":"J. Log. Comput."},{"key":"24_CR28","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. Comput. Sci. 15, 1033\u20131088 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"key":"24_CR29","unstructured":"H\u00f3u, Z.: Labelled sequent calculi and automated reasoning for assertions in separation logic. Ph.D. thesis, The Australian National University (2015)"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-319-21401-6_34","volume-title":"Automated Deduction - CADE-25","author":"Z H\u00f3u","year":"2015","unstructured":"H\u00f3u, Z., Gor\u00e9, R., Tiu, A.: Automated theorem proving for assertions in separation logic with all connectives. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 501\u2013516. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_34"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"H\u00f3u, Z., Clouston, R., Tiu, A., Gor\u00e9, R.: Proof search for propositional abstract separation logics via labelled sequents. In: Proceedings of POPL 2014, pp. 465\u2013476. ACM (2014)","DOI":"10.1145\/2535838.2535864"},{"issue":"3","key":"24_CR32","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/373243.375719","volume":"36","author":"Samin S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: Proceedings of POPL 2001, 14\u201326. ACM (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic (2017). Under consideration for publication in Journal of Functional Programming","DOI":"10.1017\/S0956796818000151"},{"issue":"2","key":"24_CR34","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1093\/logcom\/exu031","volume":"26","author":"D Larchey-Wendling","year":"2016","unstructured":"Larchey-Wendling, D.: The formal strong completeness of partial monoidal Boolean BI. J. Log. Comput. 26(2), 605\u2013640 (2016)","journal-title":"J. Log. Comput."},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: The undecidability of Boolean BI through phase semantics. In: Proceedings of LICS 2010, pp. 140\u2013149. IEEE Computer Society Press (2010)","DOI":"10.1109\/LICS.2010.18"},{"key":"24_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-662-44602-7_25","volume-title":"Theoretical Computer Science","author":"D Larchey-Wendling","year":"2014","unstructured":"Larchey-Wendling, D., Galmiche, D.: Looking at separation algebras with Boolean BI-eyes. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 326\u2013340. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44602-7_25"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Nakano, H.: A modality for recursion. In: Proceedings of LICS 2000, pp. 255\u2013266. IEEE (2000)","DOI":"10.1109\/LICS.2000.855774"},{"issue":"2","key":"24_CR38","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1093\/logcom\/exu037","volume":"26","author":"S Negri","year":"2016","unstructured":"Negri, S.: Proof analysis beyond geometric theories: from rule systems to systems of rules. J. Log. Comput. 26(2), 513\u2013537 (2016)","journal-title":"J. Log. Comput."},{"key":"24_CR39","unstructured":"O\u2019Hearn, P.: A Primer on Separation Logic. Software Safety and Security. NATO Science for Peace and Security Series, vol. 33, pp. 286\u2013318 (2012)"},{"issue":"2","key":"24_CR40","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P., Pym, D.: The logic of bunched implications. Bull. Symb. Log. 5(2), 215\u2013244 (1999)","journal-title":"Bull. Symb. Log."},{"key":"24_CR41","doi-asserted-by":"crossref","unstructured":"Park, J., Seo, J., Park, S.: A theorem prover for BBI. In: Proceedings of POPL 2013, pp. 219\u2013232. ACM (2013)","DOI":"10.1145\/2480359.2429095"},{"key":"24_CR42","unstructured":"Parkinson, M.: Local reasoning for Java. Ph.D. thesis, University of Cambridge (2005)"},{"key":"24_CR43","unstructured":"Polonsky, A.: Proofs, Types and Lambda Calculus. Ph.D. thesis, University of Bergen (2012)"},{"key":"24_CR44","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS 2002, pp. 55\u201374. IEEE Computer Society Press (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"24_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-02716-1_23","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"RA Schmidt","year":"2009","unstructured":"Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 310\u2013324. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_23"},{"key":"24_CR46","unstructured":"Simpson, A.: The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh (1994)"},{"key":"24_CR47","unstructured":"Skolem, T.: Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit und Beweisbarkeit mathematischen S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen, Skrifter I, vol. 4, pp. 1\u201336. Det Norske Videnskaps-Akademi, (1920)"},{"key":"24_CR48","unstructured":"Terese: Term Rewriting Systems. Cambridge University Press (2003)"},{"key":"24_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-10672-9_15","volume-title":"Programming Languages and Systems","author":"J Villard","year":"2009","unstructured":"Villard, J., Lozes, \u00c9., Calcagno, C.: Proving copyless message passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 194\u2013209. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_15"},{"key":"24_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/3-540-45931-6_28","volume-title":"Foundations of Software Science and Computation Structures","author":"H Yang","year":"2002","unstructured":"Yang, H., O\u2019Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 402\u2013416. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_28"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89366-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T17:34:27Z","timestamp":1751564067000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89366-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893655","9783319893662"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89366-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}