Skip to main content
SpringerLink
Log in

An Algebraic Glimpse at Bunched Implications and Separation Logic

  • Chapter
  • First Online:
Hiroakira Ono on Substructural Logics

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 23))

Abstract

We overview the logic of Bunched Implications (BI) and Separation Logic (SL) from a perspective inspired by Hiroakira Ono’s algebraic approach to substructural logics. We propose generalized BI algebras (GBI-algebras) as a common framework for algebras arising via “declarative resource reading”, intuitionistic generalizations of relation algebras and arrow logics and the distributive Lambek calculus with intuitionistic implication. Apart from existing models of BI (in particular, heap models and effect algebras), we also cover models arising from weakening relations, formal languages or more fine-grained treatment of labelled trees and semistructured data. After briefly discussing the lattice of subvarieties of \(\mathsf {GBI}\), we present a suitable duality for \(\mathsf {GBI}\) along the lines of Esakia and Priestley and an algebraic proof of cut elimination in the setting of residuated frames of Galatos and Jipsen. We also show how the algebraic approach allows generic results on decidability, both positive and negative ones. In the final part of the paper, we gently introduce the substructural audience to some theory behind state-of-art tools, culminating with an algebraic and proof-theoretic presentation of (bi-) abduction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Let us note that dropping associativity of multiplicative conjunction has also been considered from all three perspectives, i.e., that of arrow logic, that of substructural logic, and most recently that of BI and resource reasoning. See Remark 7.5 for more information.

  2. 2.

    Interestingly, the intuitionistic BI is embeddable in the classical BBI [95], rather than the other way around. Indeed, as pointed out in Litak et al. [101, Sect. 4.1], (un)decidability results discussed in Sect. 7 entail that no negative translation from BBI to BI can work.

  3. 3.

    In the theory of semigroups, one would rather use the name algebraic preordering. It is also known as divisibility relation for commutative semigroups.

  4. 4.

    Brotherston and Kanovich [19, Sect. 2.2] stick to the finite partial definition, but the total one is arguably more natural and common (see e.g. [49, 126, 147]); this is one of differences between stores (stacks) and heap(let)s. Especially under the total perspective the name store, used also by Demri and Deters [49] seems more adequate. Nevertheless, both perspectives can be brought together: one can think of the constant function \(\lambda x : PVar . 0\) as the default or unintialized stack (store) and restrict the attention to stacks almost everywhere equal to zero.

  5. 5.

    The reader is encouraged to compare this list with Galatos et al. [68, Sect. 3.5].

  6. 6.

    The need for items 8. and 9. was pointed out by Docherty and Pym, see [54, 55]. Here we use item 8. as first introduced by Urquhart [144] for relevant implication \(x\rightarrow y=y/x\), and item 9. is the corresponding version for \(\backslash \).

  7. 7.

    The proof of decidability of \(\mathsf {GBI}\) in Galatos and Jipsen [67] appears to have an issue with the complexity measure, as pointed out by R. Ramanayake. Decidability of \(\mathsf {nGBI}\) has also been proved by Docherty and Pym [54], independently of the same result in Galatos and Jipsen [67].

  8. 8.

    Needless to say, the residuated frame approach to proof theory of (G)BI is not the only possible one. As we have already pointed out, there is an intimate connection with a massive body of work on proof theory of relevance logics. See comments and references in the Introduction. We should also mention here that there are numerous more recent references, e.g., cut-free proof calculi for subvarieties of \(\mathsf {BI}\) of Ciabattoni and Ramanayake [38].

  9. 9.

    A logician may object whether the word variables is really appropriate here. Sometimes the term (storage) locations is used instead [147], but as the reader will recall, we already used this name in Sect. 3.4 for pointer labels and will continue to do so below.

  10. 10.

    Note that the assertion for WHILE is valid only when read as a partial one. That is, \(\{P\}C\{Q\}\) is read as if C is started in a store satisfying P and terminates, then any store it terminates in satisfies Q. Under this reading, for example, \(\{\top \}C\{\bot \}\) simply specifies that C never terminates, regardless of the original values of program variables. An alternative reading, usually denoted as [P]C[Q], is the total one: if C is started in a store satisfying P, then it terminates and any store it terminates in satisfies Q.

  11. 11.

    On the other hand, the semantic clause of \(\mathbin {{-}\!*}\) quantifies over the collection of all possible disjoint extensions satisfying Q, which can be infinite, and is problematic from a model checking point of view. For this reason, there is a line of research dealing with adjunct elimination for separation logic and related formalisms [25, 29, 47, 102].

  12. 12.

    When specifying this property in a proof assistant, one can do it in a (co)inductive fashion. In a metatheory allowing excluded middle at least for assertions, one can work with two inductive properties fault and no_fault and show (using excluded middle) that they are complementary, i.e., that for any (s, h) and C exactly one of the two holds. Alternatively, one can stay within constructive metatheory by making no_fault coinductive. See [123] for an example of a student-oriented formalization in a proof assistant discussing these issues.

  13. 13.

    In our ideal mathematical world, where heaps can be arbitrarily large as long as they are finite, allocation never leads to a memory fault (unlike lookup, mutation and deallocation).

  14. 14.

    Of course, only free occurrences matters. But in our language there are no binders for elements of PVar (unlike AVar).

  15. 15.

    The term frame problem was originally proposed in a classical 1969 paper [106] on problems of knowledge representation in artificial intelligence. The realization that such problems arise also in formal specifications using Floyd-Hoare logics predates the development of separation logic. An example, focusing on the issues of object-oriented specifications with inheritance, is provided by a 1995 paper by Borgida et al. [13].

  16. 16.

    Note that this rule allows to spread equality statements across the bunch. In the store-and-heap semantics, such atoms are heap-independent: they only depend on the store.

  17. 17.

    Note that the denotation of pointer atoms is finite only if both \(\textit{PVar}\) and \(\textit{Val}\) are finite. Brotherston and Kanovich [19, Sect. 10] circumvent this by stating corresponding theorems in the heap-only setting, but given that the original result of Calcagno et al. [30] was proved for a store-and-heap model, a somewhat more general formulation would be desirable.

  18. 18.

    Although when it comes to Peirce’s own views, “[i]t is a common complaint that no coherent picture emerges from Peirce’s writings on abduction. (Though perhaps this is not surprising, given that he worked on abduction throughout his career, which spanned a period of more than fifty years ...)” [56].

  19. 19.

    https://github.com/Microsoft/SLAyer.

  20. 20.

    https://github.com/facebook/infer.

References

  1. Andréka, H., Kurucz, Á., Németi, I., Sain, I., & Simon, A. (1996). Causes and remedies for undecidability in arrow logics and in multi-modal logics. In Arrow logic and multi-modal logic (pp. 63–100). Study logic, language and information. CSLI Publications.

    Google Scholar 

  2. Armeín, P. A., & Pym, D. J. (2001). Bunched logic programming. In Proceedings of IJCAR (Vol. 2083, pp. 289–304). LNCS. Springer.

    Google Scholar 

  3. Belardinelli, F., Jipsen, P., & Ono, H. (2004). Algebraic aspects of cut elimination. Studia Logica, 77(2), 209–240.

    Article  Google Scholar 

  4. Belnap, N. D., Jr. (1982). Display logic. Journal of Philosophical Logic, 11(4), 375–417.

    Article  Google Scholar 

  5. Berdine, J., Calcagno, C., & O’Hearn, P. W. (2005). A decidable fragment of separation logic. In Proceeding of FSTTCS (pp. 97–109).

    Google Scholar 

  6. Berdine, J., Calcagno, C., & O’Hearn, P. W. (2006). Smallfoot: modular automatic assertion checking with separation logic. In Proceedings of FMCO (pp. 115–137).

    Google Scholar 

  7. Berdine, J., Calcagno, C., & O’Hearn, P. W. (2005). Symbolic execution with separation logic. In Proceedings of APLAS (pp. 52–68).

    Google Scholar 

  8. Berdine, J., Cook, B., & Ishtiaq, S. (2011). Slayer: Memory safety for systems-level code. In Proceedings of CAV (pp. 178–183).

    Google Scholar 

  9. Biering, B., Birkedal, L., & Torp-Smith, N. (2007). BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Transactions on Programming Languages and Systems, 29(5) (2007).

    Google Scholar 

  10. Blok, W. J., & Pigozzi, D. (1989). Algebraizable logics (Vol. 77). Memoirs AMS 396. AMS.

    Google Scholar 

  11. Blok, W. J., & Van Alten, C. J. (2002). The finite embeddability property for residuated lattices, pocrims and BCK-algebras. Algebra University, 48(3), 253–271.

    Article  Google Scholar 

  12. Bloom, S. L., & Ésik, Z. (1993). Iteration theories: The equational logic of iterative processes. Monographs in theoretical computer science. An EATCS series. Springer.

    Google Scholar 

  13. Borgida, A., Mylopoulos, J., & Reiter, R. (1995). On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10), 785–798.

    Article  Google Scholar 

  14. Bornat, R. (2000). Proving pointer programs in Hoare logic. In Proceedings of MPC (pp. 102–126).

    Google Scholar 

  15. Bornat, R., Calcagno, C., & Yang, H. (2006). Variables as resource in separation logic. In Proceedings of MFPS (Vol. 155, pp. 247–276). ENTCS.

    Google Scholar 

  16. Brookes, S. (2007). A semantics for concurrent separation logic. Theoretical Computer Science, 375(1–3), 227–270.

    Article  Google Scholar 

  17. Brookes, S., & O’Hearn, P. W. (2016). Concurrent separation logic. ACM SIGLOG News, 3(3), 47–65.

    Article  Google Scholar 

  18. Brotherston, J., & Calcagno, C. (2010). Classical BI: Its semantics and proof theory. LMCS (Vol. 6.3).

    Google Scholar 

  19. Brotherston, J., & Kanovich, M. (2014). Undecidability of propositional separation logic and its neighbours. Journal of ACM, 61(2), 14:1–14:43.

    Google Scholar 

  20. Brotherston, J.,& Kanovich, M. I. (2010). Undecidability of propositional separation logic and its neighbours. In Proceedings of LiCS (pp. 130–139).

    Google Scholar 

  21. Brotherston, J., & Villard, J. (2014). Parametric completeness for separation theories (pp. 453–464).

    Google Scholar 

  22. Bürckert H.-J. (1986). Some relationships between unification, restricted unification, and matching. In Proceedings of CADE (pp. 514–524).

    Google Scholar 

  23. Burstall, R. M. (1972). Some techniques for proving correctness of programs which alter data structures. In Machine intelligence (Vol. 7, pp. 23–50); Edinburgh.

    Google Scholar 

  24. Calcagno, C. , O’Hearn, P. W., & Yang, H. (2007). Local action and abstract separation logic. In Proceedings of LiCS (pp. 366–378).

    Google Scholar 

  25. Calcagno, C., Dinsdale-Young, T., & Gardner, P. (2010). Adjunct elimination in context logic for trees. Information and Computation, 208(5), 474–499.

    Article  Google Scholar 

  26. Calcagno, C., & Distefano, D. (2011). Infer: An automatic program verifier for memory safety of C programs. In Proceedings of NFM (pp. 459–465).

    Google Scholar 

  27. Calcagno, C., Distefanom, D., O’Hearn, P. W., & Yang, H. (2011). Compositional shape analysis by means of bi-abduction. Journal ACM, 58(6), 26:1–26:66.

    Google Scholar 

  28. Calcagno, C., Gardner, P., & Zarfaty, U. (2005). Context logic and tree update. In Proceedings of POPL (pp. 271–282).

    Google Scholar 

  29. Calcagno, C., Gardner, P., & Zarfaty, U. (2007). Context logic as modal logic: Completeness and parametric inexpressivity. In Proceedings of POPL (pp. 123–134).

    Google Scholar 

  30. Calcagno, C., Yang, H., & O’Hearn, P. W. (2001). Computability and complexity result for a spatial assertion language for data structures. In Proceedings of FSTTCS (pp. 108–119).

    Google Scholar 

  31. Calcagno, C., et al. (2015). Moving fast with software verification. In Proceedings of NFM (pp. 3–11).

    Google Scholar 

  32. Cardelli, L., & Ghelli, G. (2004). TQL: A query language for semistructured data based on the ambient logic. In MSCS 14 (03 2004) (pp. 285–327).

    Google Scholar 

  33. Cardelli, L., & Gordon, A. D. (2000). Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of POPL (pp. 365–377).

    Google Scholar 

  34. ten Cate, B., Fontaine, G., & Litak, T. (2010). Some modal aspects of XPath. Journal of Applied Non-Classical Logics, 20(3), 139–171.

    Article  Google Scholar 

  35. ten Cate, B., Litak, T., & Marx, M. (2010). Complete axiomatizations for XPath fragments. Journal of Applied Logics, 8(2), 153–172.

    Article  Google Scholar 

  36. Chagrov, A., & Zakharyaschev, M. (1997). Modal logic. Oxford Logic Guides (Vol. 35). Clarendon Press.

    Google Scholar 

  37. Chlipala, A. (2016). Formal reasoning about programs. Online book and course material: http://adam.chlipala.net/frap/.

  38. Ciabattoni, A., & Ramanayake, R. (2017). Bunched hypersequent calculi for distributive substructural logics. In Proceedings of LPAR (Vol. 46). EPiC Series in Computing (pp. 417–434).

    Google Scholar 

  39. Cintula, P., & Noguera, C. (2010). Implicational (semilinear) logics I: A new hierarchy. Archive for Mathematical Logic, 49(4), 417–446.

    Article  Google Scholar 

  40. Clarke, E. M. (1985). The characterization problem for Hoare logics. In Proceedings of a discussion meeting of the royal society of london on mathematical logic and programming languages (pp. 89–106).

    Google Scholar 

  41. Collinson, M., McDonald, K., & Pym, D. (2014). A substructural logic for layered graphs. Journal of Logic and Computation, 24(4), 953–988.

    Article  Google Scholar 

  42. Cook, S. A. (1978). Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1), 70–90.

    Article  Google Scholar 

  43. Cuoq, P., et al. (2012). Frama-c. In Proceedings of SEFM (pp. 233–247).

    Google Scholar 

  44. Dang, H.-H., Höfner, P., & Möller, B. (2011). Algebraic separation logic. JLAMP, 80(6), 221–247.

    Article  Google Scholar 

  45. Davey, B. A., & Galati, J. C. (2003). A coalgebraic view of Heyting duality. Studia Logica, 75, 259–270.

    Article  Google Scholar 

  46. Davey, B. A., & Priestley, H. A. (2002). Introduction to lattices and order. Cambridge.

    Book  Google Scholar 

  47. Dawar, A., Gardner, P., & G. Ghelli (2004). Adjunct elimination through games in static ambient logic. In Proceedings of FSTTCS (pp. 211–223).

    Google Scholar 

  48. Day, B. (1970). On closed categories of functors. In: Reports of the midwest category seminar IV. (Vol. 137). Lecture Notes in Mathematics (pp. 1–38).

    Google Scholar 

  49. Demri, S., & Deters, M. (2015). Separation logics and modalities: A survey. Journal of Applied Non-Classical Logics.

    Google Scholar 

  50. Demri, S., & Deters, M. (2015). Two-variable separation logic and its inner circle. ACM Transactions on Computational Logic, 16(2), 15:1–15:36.

    Google Scholar 

  51. Demri, S., Galmiche, D., Larchey-Wendling, D., & Méry, D. (2014). Separation logic with one quantified variable. In Proceedings of CSR (pp. 125–138).

    Google Scholar 

  52. Denecker, M., & Kakas, A. (2000). Special issue: Abductive logic programming. Journal Logic Programming, 44(1), 1–4.

    Article  Google Scholar 

  53. Distefano, D., O’Hearn, P. W., & Yang, H. (2006). A local shape analysis based on separation logic. In Proceedings of TACAS (pp. 287–302).

    Google Scholar 

  54. Docherty, S., & Pym, D. J. (2017). Intuitionistic layered graph logic: Semantics and proof theory. CoRR. arXiv:1710.03021.

  55. Docherty, S. & Pym, D. J. (2017). Stone-type dualities for separation logics. CoRR. arXiv:1710.03021.

  56. Douven, I. (2017). Abduction. In The Stanford encyclopedia of philosophy. Metaphysics Research Lab, Stanford U. https://plato.stanford.edu/archives/sum2017/entries/abduction/.

  57. Dunn, J. M. (1975). Consecution formulation of positive R with co-tenability and t. In Entailment: The logic of relevance and necessity (Vol. 1, pp. 381–391). Princeton.

    Google Scholar 

  58. Engberg, U., & Winskel, G. (1997). Completeness results for linear logic on Petri nets. Annals of Pure and Applied Logic, 86(2), 101–135.

    Article  Google Scholar 

  59. Floyd, R. W. (1967). Assigning meanings to programs. In Mathematical aspects of computer science (Vol. 19, pp. 19–32); Proceedings of Symposia in Applied Mathematics AMS.

    Google Scholar 

  60. Font, J. M. (2018). Abstract algebraic logic. An introductory chapter. In Hiroakira Ono on residuated lattices and substructural logics. Outstanding contributions to logic. Springer (to appear).

    Google Scholar 

  61. Foulis, D. J., & Bennett, M. K. (1994). Effect algebras and unsharp quantum logics. Foundations of Physics, 24(10), 1331–1352.

    Article  Google Scholar 

  62. Freese, R. (1980). Free modular lattices. Transactions of the American Mathematical Society, 261(1), 81–91.

    Article  Google Scholar 

  63. Galatos, N. (2005). Minimal varieties of residuated lattices. Algebra University, 52(2), 215–239.

    Article  Google Scholar 

  64. Galatos, N. (2000). Selected topics on residuated lattices (p. 50). Qualifying paper: Department of Mathematics, Vanderbilt U.

    Google Scholar 

  65. Galatos, N. (2002). The undecidability of the word problem for distributive residuated lattices. In Developments in mathematics (Vol. 7, pp. 231–243).

    Google Scholar 

  66. Galatos, N., & Jipsen, P. (2013). Residuated frames with applications to decidability. Transactions of the American Mathematical Society, 365(3), 1219–1249.

    Article  Google Scholar 

  67. Galatos, N.,& Jipsen, P., (March, 2017). Distributive residuated frames and generalized bunched implication algebras. Algebra University, 78, 303–336.

    Google Scholar 

  68. Galatos, N., Jipsen, P., Kowalski, T., & Ono, H. (2007). Residuated lattices: An algebraic glimpse at substructural logics. Studies in Logic and the Foundations of Mathematics, 151.

    Google Scholar 

  69. Galatos, N., & Jipsen, P. (2020). The structure of generalized BI-algebras and weakening relation algebras. Algebra Universalis, 81(3), 1–35. https://doi.org/10.1007/s00012-020-00663-9.

  70. Galatos, N., & Jipsen, P. (2020). Weakening relation algebras and FL\({}^{\text{2}}\)-algebras. In U. Fahrenberg, P. Jipsen, & M. Winter (Eds.), Relational and algebraic methods in computer science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8–11, 2020, Proceedings, Lecture Notes in Computer Science. Vol. 12062, pp. 117–133. https://doi.org/10.1007/978-3-030-43520-2_8.

  71. Galatos, N., & Ono, H. (2010). Cut elimination and strong separation for substructural logics: An algebraic approach. Annals of Pure and Applied Logic, 161(9), 1097–1133.

    Article  Google Scholar 

  72. Galatos, N., & Raftery, J. G. (2004). Adding involution to residuated structures. Studia Logica, 77(2), 181–207.

    Article  Google Scholar 

  73. Galmiche, D., & Larchey-Wendling, D. (2006). Expressivity properties of boolean BI through relational models. In Proceedings of FSTTCS (pp. 357–368).

    Google Scholar 

  74. Galmiche, D., Méry, D., & Pym, D. J. (2005). The semantics of BI and resource tableaux. MSCS, 15(6), 1033–1088.

    Google Scholar 

  75. Henkin, L., Monk, J., & Tarski, A. (1985). Cylindric algebras. Part II. Studies in Logic and the Foundations of Mathematics (Vol. 115). North-Holland.

    Google Scholar 

  76. Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576–580.

    Article  Google Scholar 

  77. Hoare, T., Möller, B., Struth, G., & Wehrman, I. (2011). Concurrent Kleene algebra and its foundations. JLAMP, 80(6), 266–296.

    Google Scholar 

  78. Ishtiaq, S. S., & O’Hearn, P. W. (2001). BI as an assertion language for mutable data structures. In Proceedings of POPL (pp. 14–26).

    Google Scholar 

  79. Jacobs, B., Vogels, F., & Piessens, F. (2015). Featherweight VeriFast. LMCS (Vol. 11) (2015).

    Google Scholar 

  80. Jacobs, B., et al. (2011) VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of NFM (pp. 41–55).

    Google Scholar 

  81. Jankov, V. A. (1968). The construction of a sequence of strongly independent superintuitionistic propositional calculi. Soviet Mathematics Doklady, 9,.

    Google Scholar 

  82. Jipsen, P. (1992). Computer-aided investigations of relation algebras. PhD thesis. Vanderbilt U.

    Google Scholar 

  83. Jipsen, P. (2014). Concurrent Kleene algebra with tests. In Proceedings of RAMiCS (Vol. 8428, pp. 37–48). LNCS.

    Google Scholar 

  84. Jipsen, P., & Maddux, R. (1997). Nonrepresentable sequential algebras. Logic Journal of the IGPL, 5(4), 565–574.

    Article  Google Scholar 

  85. Jipsen, P., & Moshier, M. A. (2016). Concurrent Kleene algebra with tests and branching automata. JLAMP, 85(4), 637–652.

    Google Scholar 

  86. Jipsen, P., & Tsinakis, C. (2002). A survey of residuated lattices. In Developments in Mathematics (Vol. 7, pp. 19–56).

    Google Scholar 

  87. Jónsson, B., & Tsinakis, C. (1993). Relation algebras as residuated boolean algebras. Algebra University, 30(4), 469–478.

    Article  Google Scholar 

  88. Jung, R., Krebbers, R., Birkedal, L., & Dreyer, D. (2016). Higher-order ghost state. In Proceedings of ICFP (pp. 256–269).

    Google Scholar 

  89. Kassios, I. T. (2006). Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Proceedings of FM (pp. 268–283).

    Google Scholar 

  90. Kleymann, T. (1999). Hoare logic and auxiliary variables. Formal Aspects of Computing, 11(5), 541–566.

    Article  Google Scholar 

  91. Kozak, M. (2009). Distributive full Lambek calculus has the finite model property. Studia Logica, 91(2), 201–216.

    Article  Google Scholar 

  92. Kozen, D. (2000). On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic, 1(1), 60–76.

    Article  Google Scholar 

  93. Krebbers, R., et al. (2018). MoSeL: A general, extensible modal framework for interactive proofs in separation logic. In Proceedings of ACM Programming Languages, 2. ICFP (pp. 77:1–77:30).

    Google Scholar 

  94. Kurucz, Á., Németi, I., Sain, I., & Simon, A. (1995). Decidable and undecidable logics with a binary modality. JoLLI, 4(3), 191–206.

    Article  Google Scholar 

  95. Larchey-Wendling, D., & Galmiche, D. (2009). Exploring the relation between Intuitionistic BI and Boolean BI: An unexpected embedding. MSCS, 19(3), 435–500.

    Google Scholar 

  96. Larchey-Wendling, D., & Galmiche, D. (2013). Nondeterministic phase semantics and the undecidability of boolean BI. ACM Transactions on Computational Logic, 14(1), 6:1–6:41.

    Google Scholar 

  97. Larchey-Wendling, D., & Galmiche, D. (2010). The undecidability of boolean BI through phase semantics. In Proceedings of LiCS (pp. 140–149).

    Google Scholar 

  98. Leino, K. R. M. (2010). Dafny: An automatic program verifier for functional correctness. In Proceedings of LPAR (pp. 348–370). Berlin: Springer.

    Google Scholar 

  99. Lipshitz, L. (1974). The undecidability of the word problems for projective geometries and modular lattices. Transactions of the American Mathematical Society, 193, 171–180.

    Article  Google Scholar 

  100. Litak, T. (2013–2018.). Lecture material of SemProg 2018@FAU: our fork of [122]. http://dx.doi.org/10.13140/RG.2.2.10542.36168.

  101. Litak, T., Polzer, M., & Rabenstein, U. (2017). Negative translations and normal modality. In Proceedings of FSCD (Vol. 84, 27:1–27:18). LIPIcs.

    Google Scholar 

  102. Lozes, É. (2004). Adjuncts elimination in the static ambient logic. In Proceedings of the 10th international workshop on expressiveness in concurrency (Vol. 96, pp. 51–72); ENTCS.

    Google Scholar 

  103. Maddux, R. D. (2006). Relation algebras. Studies in logic and the foundations of mathematics (Vol. 150).

    Google Scholar 

  104. Manes, E. G., & Arbib, M. A. (1986). Algebraic approaches to program semantics. The AKM series in theoretical CS.

    Google Scholar 

  105. Marx, M., Pólos, L., & Masuch, M. (Eds). Arrow logic and multi-modal logic. Studies in logic, language, and information. CSLI Publications.

    Google Scholar 

  106. McCarthy, J., & Hayes, P. J. (1969). Some philosophical problems from the standpoint of artificial intelligence. In Machine intelligence (Vol. 4, pp. 463–502); Edinburgh.

    Google Scholar 

  107. McKinsey, J. C. C., & Tarski, A. (1946). On closed elements in closure algebras. Annals of Mathematics, 47(1), 122–162.

    Article  Google Scholar 

  108. Meyer, B. (1997). Object-oriented software construction (2nd ed.). Prentice-Hall, Inc.

    Google Scholar 

  109. Mikulás, S. (1996). Complete calculus for conjugated arrow logic. In: Arrow logic and multi-modal logic. Studies in logic, language, and information (pp. 125–139). CSLI Publications.

    Google Scholar 

  110. Mints, G. E. (1976). Cut-elimination theorem for relevant logics. Journal of Soviet Mathematics, 6(4), 422–428.

    Article  Google Scholar 

  111. von Neumann, J. (1960). Continuous geometry. Princeton.

    Google Scholar 

  112. O’Hearn, P. W. (2012). A primer on separation logic (and automatic program verification and analysis). In Software safety and security (Vol. 33, pp. 286–318). NATO SPS Series D.

    Google Scholar 

  113. O’Hearn, P. W. (2017). Email to T. Litak and P. Jipsen, 29 August 2017.

    Google Scholar 

  114. O’Hearn, P. W. (1999). Resource interpretations, bunched implications and the al-calculus (preliminary version). In Proceedings of TLCA (Vol. 1581, pp. 258–279). LNCS.

    Google Scholar 

  115. O’Hearn, P. W. (2007). Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1), 271–307.

    Article  Google Scholar 

  116. O’Hearn, P. W., Petersen, R. L., Villard, J., & Hussain, A. (2015). On the relation between concurrent separation logic and concurrent kleene algebra. JLAMP, 84(3), 285–302.

    Google Scholar 

  117. O’Hearn, P. W., & Pym, D. J. (1999). The logic of bunched implications. 5.2, 215–244.

    Google Scholar 

  118. O’Hearn, P. W., Yang, H., & Reynolds, J. C. (2009). Separation and information hiding. ACM Transactions on Programming Languages and Systems, 31(3), 1–50.

    Article  Google Scholar 

  119. O’Hearn, P., Reynolds, J., & Yang, H. (2001). Local reasoning about programs that alter data structures. In Proceedings of CSL (pp. 1–19).

    Google Scholar 

  120. Parkinson, M., Bornat, R., & Calcagno, C. (2006). Variables as resource in Hoare logics. In Proceedings of LiCS (pp. 137–146).

    Google Scholar 

  121. Parkinson, M., & Bierman, G. (2005). Separation logic and abstraction. In Proceedings Of POPL (pp. 247–258).

    Google Scholar 

  122. Paul, G. (1993). Approaches to abductive reasoning: An overview. Artificial Intelligence Review, 7(2), 109–152.

    Article  Google Scholar 

  123. Paulus, D. (2016). ImpDynamic: Dynamic memory allocation and separation logic in the style of Software Foundations. A Coq formalization supervised by T. Litak, part of plf18 volume of [96]

    Google Scholar 

  124. Peirce, C. S. (1931–1958). In C. Hartshorne, P. Weiss, and A. B. Harvard (Eds.), Collected papers of charles sanders peirce.

    Google Scholar 

  125. Philippaerts, P., et al. (2014). Software verification with VeriFast: Industrial case studies. Science of Computer Programming, 82, 77–97.

    Article  Google Scholar 

  126. Pierce, B. C. et al. (2018) Software foundations. Version 5.6 (25 Aug 2018, Coq 8.8.0). Electronic textbook http://www.cis.upenn.edu/~cpierce/sf.

  127. Pratt, V. (1991). Action logic and pure induction. In Logics in AI (Vol. 478, pp. 97–120). LNCS.

    Google Scholar 

  128. Pratt, V. R. (1976). Semantical consideration on Floyd-Hoare logic. In Proceedings of the 17th SFCS (pp. 109–121).

    Google Scholar 

  129. Pym, D. (2002). The semantics and proof theory of the logic of bunched implications (Vol. 26). Applied logic series: Kluwer Academic Publishers.

    Google Scholar 

  130. Pym, D. J. (1999). On bunched predicate logic. In Proceedings of LiCS (pp. 183–192).

    Google Scholar 

  131. Pym, D. J., O’Hearn, P. W., & Yang, H. (2004). Possible worlds and resources: The semantics of BI. Theoretical Computer Science, 315(1), 257–305.

    Article  Google Scholar 

  132. Raftery, J. (2018). Universal algebraic methods for non-classical logics. In Hiroakira Ono on residuated lattices and substructural logics. Outstanding contributions to logic. Springer (to appear).

    Google Scholar 

  133. Ramanayake, R. (2016). A purely syntactic proof of decidability for BI. CoRR. arXiv:1609.05847.

  134. Rasiowa, H. (1974). An algebraic approach to non-classical logics (Vol. 78). Studies in logic and the foundations of mathematics. North-Holland.

    Google Scholar 

  135. Read, S. (1988). Relevant logic: A philosophical examination of inference. B. Blackwell.

    Google Scholar 

  136. Reynolds, J. C. (2000). Intuitionistic reasoning about shared mutable data structure. In Millennial perspectives in computer science (pp. 303–321); Palgrave.

    Google Scholar 

  137. Reynolds, J. C. (2002). Separation logic: A logic for shared mutable data structures. In Proceedings of LiCS (pp. 55–74).

    Google Scholar 

  138. Sieczkowski, F., Bizjak, A., & Birkedal, L. (2015). ModuRes: A Coq library for modular reasoning about concurrent higher-order imperative programming languages. In Proceedings of ITP (pp. 375–390).

    Google Scholar 

  139. Smans, J., Jacobs, B., & Piessens, F. (2009). Implicit dynamic frames: combining dynamic frames and separation logic. In Proceedings of ECOOP (pp. 148–172).

    Google Scholar 

  140. Tarski, A. (1941). On the calculus of relations. Journal of Symbolic Logic, 6(3), 73–89.

    Article  Google Scholar 

  141. Troelstra, A., & Schwichtenberg, H. (1996). Basic proof theory. Cambridge.

    Google Scholar 

  142. Tuerk, T. (2011). A separation logic framework for HOL. Technical report UCAM-CL-TR-799. University of Cambridge, Computer Laboratory.

    Google Scholar 

  143. Urquhart, A. (1995). Decision problems for distributive lattice-ordered semigroups. Algebra University, 33(3), 399–418.

    Article  Google Scholar 

  144. Urquhart, A. (1996). Duality for algebras of relevant logics. Studia Logica, 56, 1–2 ; Special issue on Priestley duality, pp. 263–276.

    Google Scholar 

  145. Urquhart, A. (1972). Semantics for relevant logics. Journal of Symbolic Logic, 37(1), 159–169.

    Article  Google Scholar 

  146. Urquhart, A. (1984). The undecidability of entailment and relevant implication. Journal of Symbolic Logic, 49(4), 1059–1073.

    Article  Google Scholar 

  147. Winskel, G. (1993). The formal semantics of programming languages: An introduction. MIT Press.

    Google Scholar 

  148. Yang, H. (2001). Local reasoning for stateful programs. PhD thesis. University of Illinois.

    Google Scholar 

  149. Yang, H., et al. (2008) Scalable shape analysis for systems code. In Proceedings of CAV (pp. 385–398).

    Google Scholar 

Download references

Acknowledgements

We would like to thank: Hiroakira Ono, without whom both authors would not have met once upon a time in western Japan, there would have been no stimulus to write this overview, and many other things would not have happened; Nick Galatos and Kazushige Terui for suggesting the idea to write this overview, and for their patience and support during the very long write-up period; Nick, Peter O’Hearn, Revantha Ramanayake and Simon Docherty for their comments in the final stages of write-up, in Peter’s case including the suggestion to add some material on bi-abduction (Sect. 11) and feedback regarding Infer and automated tools discussed in Sect. 12.2. Moreover, the second author wishes to thank: the family of the first author, in particular Julie Tapp, for hosting him for two weeks in April 2015, when the bulk of this paper was written; his project student Dominik Paulus for developing a convenient Coq formalization [123], which proved helpful when working on Sects. 9–10; and Erwin R. Catesbeiana, for displaying a tantalizing view on the empty heaplet.

Author information

Authors and Affiliations

  1. School of Computational Sciences, Chapman University, Orange, USA

    Peter Jipsen

  2. Informatik 8, FAU Erlang-en-Nürnberg, Erlangen, Germany

    Tadeusz Litak

Authors
  1. Peter Jipsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tadeusz Litak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Jipsen .

Editor information

Editors and Affiliations

  1. Department of Mathematics, University of Denver, Denver, CO, USA

    Nikolaos Galatos

  2. Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan

    Kazushige Terui

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Jipsen, P., Litak, T. (2022). An Algebraic Glimpse at Bunched Implications and Separation Logic. In: Galatos, N., Terui, K. (eds) Hiroakira Ono on Substructural Logics. Outstanding Contributions to Logic, vol 23. Springer, Cham. https://doi.org/10.1007/978-3-030-76920-8_5

Download citation

Publish with us

Policies and ethics

Search

Navigation