Document Open Access Logo

Sub-classical Boolean Bunched Logics and the Meaning of Par

Authors James Brotherston, Jules Villard

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.325.pdf
  • Filesize: 0.5 MB
  • 18 pages

Document Identifiers

Author Details

James Brotherston
Jules Villard

Cite As Get BibTex

James Brotherston and Jules Villard. Sub-classical Boolean Bunched Logics and the Meaning of Par. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 325-342, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.325

Abstract

We investigate intermediate logics between the bunched logics Boolean BI and Classical BI, obtained by combining classical propositional logic with various flavours of Hyland and De Paiva's full intuitionistic linear logic. Thus, in addition to the usual multiplicative conjunction (with its adjoint implication and unit), our logics also feature a multiplicative disjunction (with its adjoint co-implication and unit). The multiplicatives behave "sub-classically", in that disjunction and conjunction are related by a weak distribution principle, rather than by De Morgan equivalence.

We formulate a Kripke semantics, covering all our sub-classical bunched logics, in which the multiplicatives are naturally read in terms of resource operations. Our main theoretical result is that validity according to this semantics coincides with provability in a corresponding Hilbert-style proof system.

Our logical investigation sheds considerable new light on how one can understand the multiplicative disjunction, better known as linear logic's "par", in terms of resource operations. In particular, and in contrast to the earlier Classical BI, the models of our logics include the heap-like memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps.

Subject Classification

Keywords
  • Bunched logic
  • linear logic
  • modal logic
  • Kripke semantics
  • model theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Nuel D. Belnap, Jr. Display logic. Journal of Philosophical Logic, 11:375-417, 1982. Google Scholar
  2. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001. Google Scholar
  3. James Brotherston. Bunched logics displayed. Studia Logica, 100(6):1223-1254, 2012. Google Scholar
  4. James Brotherston and Cristiano Calcagno. Classical BI: Its semantics and proof theory. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  5. James Brotherston and Jules Villard. Bi-intuitionistic boolean bunched logic. Technical Report RN/14/06, University College London, 2014. Google Scholar
  6. James Brotherston and Jules Villard. Parametric completeness for separation theories. In Proc. POPL-41, pages 453-464. ACM, 2014. Google Scholar
  7. Cristiano Calcagno, Dino Distefano, Peter O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. Journal of the ACM, 58(6), December 2011. Google Scholar
  8. Cristiano Calcagno, Philippa Gardner, and Uri Zarfaty. Context logic as modal logic: Completeness and parametric inexpressivity. In Proc. POPL-34, pages 123-134. ACM, 2007. Google Scholar
  9. Ranald Clouston, Jeremy Dawson, Rajeev Goré, and Alwen Tiu. Annotation-free sequent calculi for full intuitionistic linear logic. In Proc. CSL-22, pages 197-214. Dagstuhl, 2013. Google Scholar
  10. Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebras and share accounting. In Proc. APLAS-7, pages 161-177. Springer, 2009. Google Scholar
  11. Didier Galmiche and Dominique Larchey-Wendling. Expressivity properties of Boolean BI through relational models. In Proc. FSTTCS-26, pages 357-368. Springer, 2006. Google Scholar
  12. Philippa Gardner, Sergio Maffeis, and Gareth David Smith. Towards a program logic for JavaScript. In Proc. POPL-39, pages 31-44, 2012. Google Scholar
  13. Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In Proc. TAPSOFT, pages 52-66. Springer-Verlag, 1987. Google Scholar
  14. Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis. Proving that non-blocking algorithms don't block. In Proc. POPL-36, pages 16-28. ACM, 2009. Google Scholar
  15. Aquinas Hobor and Jules Villard. The ramifications of sharing in data structures. In Proc. POPL-40, pages 523-536. ACM, 2013. Google Scholar
  16. Martin Hyland and Valeria de Paiva. Full intuitionistic linear logic (extended abstract). Annals of Pure and Applied Logic, 64(3):273-–291, 1993. Google Scholar
  17. Samin Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Proc. POPL-28, pages 14-26. ACM, 2001. Google Scholar
  18. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. Google Scholar
  19. David Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer, 2002. Google Scholar
  20. David Pym, Peter O'Hearn, and Hongseok Yang. Possible worlds and resources: The semantics of BI. Theor. Comp. Sci., 315(1):257-305, 2004. Google Scholar
  21. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS-17, pages 55-74. IEEE, 2002. Google Scholar
  22. H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. O'Hearn. Scalable shape analysis for systems code. In Proc. CAV-20, pages 385-398. Springer, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact