Abstract
In this paper, we show that the formulæ of Boolean BI cannot distinguish between some of the different notions of separation algebra found in the literature: partial commutative monoids, either cancellative or not, with a single unit or not, all define the same notion of validity. We obtain this result by the careful study of the specific properties of the counter-models that are generated by tableaux proof-search in Boolean BI.
Work partially supported by the ANR grant DynRes (project No. ANR-11-BS02-011).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Brotherston, J.: Bunched Logics Displayed. Studia Logica 100(6), 1223–1254 (2012)
Brotherston, J., Kanovich, M.: Undecidability of Propositional Separation Logic and Its Neighbours. In: LICS, pp. 130–139. IEEE Computer Society (2010)
Brotherston, J., Kanovich, M.: Undecidability of Propositional Separation Logic and its Neighbours. Journal of the ACM 61(2) (2014)
Brotherston, J., Villard, J.: Parametric Completeness for Separation Theories. In: POPL, pp. 453–464. ACM (2014)
Calcagno, C., O’Hearn, P.W., Yang, H.: Local Action and Abstract Separation Logic. In: LICS, pp. 366–378. IEEE Computer Society (2007)
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL, pp. 287–300. ACM (2013)
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–177. Springer, Heidelberg (2009)
Galmiche, D., Larchey-Wendling, D.: Expressivity properties of Boolean BI through Relational Models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 357–368. Springer, Heidelberg (2006)
Hóu, Z., Clouston, R., Goré, R., Tiu, A.: Proof search for propositional abstract separation logics via labelled sequents. In: POPL, pp. 465–476. ACM (2014)
Hóu, Z., Tiu, A., Goré, R.: A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 172–187. Springer, Heidelberg (2013)
Ishtiaq, S.S., O’Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: POPL, London, UK, pp. 14–26 (2001)
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
Larchey-Wendling, D., Galmiche, D.: Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding. Mathematical Structures in Computer Science 19(3), 435–500 (2009)
Larchey-Wendling, D., Galmiche, D.: The Undecidability of Boolean BI through Phase Semantics. In: LICS, pp. 140–149. IEEE Computer Society (2010)
Larchey-Wendling, D., Galmiche, D.: Nondeterministic Phase Semantics and the Undecidability of Boolean BI. ACM ToCL 14(1), 6 (2013)
Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL, pp. 219–232. ACM (2013)
Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Kluwer Academic Publishers (2002)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Larchey-Wendling, D., Galmiche, D. (2014). Looking at Separation Algebras with Boolean BI-eyes. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds) Theoretical Computer Science. TCS 2014. Lecture Notes in Computer Science, vol 8705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44602-7_25
Download citation
DOI: https://doi.org/10.1007/978-3-662-44602-7_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44601-0
Online ISBN: 978-3-662-44602-7
eBook Packages: Computer ScienceComputer Science (R0)