Classical BI: a logic for reasoning about dualising resources

ABSTRACT

We show how to extend O'Hearn and Pym's logic of bunched implications, BI, to classical BI (CBI), in which both the additive and the multiplicative connectives behave classically. Specifically, CBI is a non-conservative extension of (propositional) Boolean BI that includes multiplicative versions of falsity, negation and disjunction. We give an algebraic semantics for CBI that leads us naturally to consider resource models of CBI in which every resource has a unique dual. We then give a cut-eliminating proof system for CBI, based on Belnap's display logic, and demonstrate soundness and completeness of this proof system with respect to our semantics.

REFERENCES

• 1: Nuel D. Belnap, Jr. Display logic. Journal of Philosophical Logic, 11:375--417, 1982.
• 2: Josh Berdine and Peter O'Hearn. Strong update, disposal and encapsulation in bunched typing. In Proceedings of MFPS, ENTCS. Elsevier, 2006.
• 3: Patrick Blackburn , Maarten de Rijke , Yde Venema, Modal logic, Cambridge University Press, New York, NY, 2001
• 4: Richard Bornat , Cristiano Calcagno , Peter O'Hearn , Matthew Parkinson, Permission accounting in separation logic, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.259-270, January 12-14, 2005, Long Beach, California, USA
• 5: James Brotherston and Cristiano Calcagno. Algebraic models and complete proof calculi for classical BI. Technical Report 2008/7, Imperial College London, 2008. Available from http://www.doc.ic.ac.uk/~jbrother.
• 6: James Brotherston and Cristiano Calcagno. Classical logic of bunched implications. In the informal proceedings of CL&C 2008, an ICALP satellite workshop; available from http://www.doc.ic.ac.uk/~jbrother, 2008.
• 7: Cristiano Calcagno , Dino Distefano , Peter O'Hearn , Hongseok Yang, Compositional shape analysis by means of bi-abduction, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 8: Cristiano Calcagno , Philippa Gardner , Uri Zarfaty, Context logic as modal logic: completeness and parametric inexpressivity, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 9: Cristiano Calcagno, Matthew Parkinson, and Viktor Vafeiadis. Modular safety checking for fine-grained concurrency. In SAS, 2007.
• 10: Bor-Yuh Evan Chang , Xavier Rival, Relational inductive shape analysis, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 11: Wei-Ngan Chin , Cristina David , Huu Hai Nguyen , Shengchao Qin, Enhancing modular OO verification with separation logic, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 12: Matthew Collinson, David Pym, and Edmund Robinson. Bunched polymorphism. Mathematical Structures in Computer Science, 2009.
• 13: Dino Distefano , Matthew J. Parkinson J, jStar: towards practical verification for java, Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications, October 19-23, 2008, Nashville, TN, USA
• 14: Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, and Sungwoo Park. The inverse method for the logic of bunched implications. In Proceedings of LPAR 2004, volume 3452 of LNAI, pages 466--480. Springer-Verlag, 2005.
• 15: Michael Dunn. Star and perp: Two treatments of negation. Philosophical Perspectives, 7:331--357, 1993.
• 16: D. Galmiche , D. Méry , D. Pym, The semantics of BI and resource tableaux, Mathematical Structures in Computer Science, v.15 n.6, p.1033-1088, December 2005 [doi>10.1017/S0960129505004858]
• 17: Didier Galmiche and Dominique Larchey-Wendling. Expressivity properties of Boolean BI through relational In Proceedings of FSTTCS, 2006.
• 18: Jean-Yves Girard. Linear logic: Its syntax and semantics.
• 19: Proceedings of the workshop on Advances in linear logic, June 1995
• 20: Rajeev Goré, Cut-free Display Calculi for Relation Algebras, Selected Papers from the10th International Workshop on Computer Science Logic, p.198-210, September 21-27, 1996
• 21: Rajeev Gore. Substructural logics on display. Logic Journal of the IGPL, 6(3):451--504, 1998.
• 22: Hongseok Yang , Oukseh Lee , Josh Berdine , Cristiano Calcagno , Byron Cook , Dino Distefano , Peter O'Hearn, Scalable Shape Analysis for Systems Code, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_36]
• 23: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 24: Huu Hai Nguyen , Wei-Ngan Chin, Enhancing Program Verification with Lemmas, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_34]
• 25: P.W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215--244, June 1999.
• 26: Matthew J. Parkinson , Gavin M. Bierman, Separation logic, abstraction and inheritance, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 27: David Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer, 2002. Errata and remarks (Pym 2004) maintained at http://www.cs.bath.ac.uk/ pym/reductive-logic-errata.html.
• 28: David J. Pym , Peter W. O'Hearn , Hongseok Yang, Possible worlds and resources: the semantics of BI, Theoretical Computer Science, v.315 n.1, p.257-305, 5 May 2004 [doi>10.1016/j.tcs.2003.11.020]
• 29: S. Read. Relevant Logic: A Philosophical Examination. Basil Blackwell, 1987.
• 30: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 31: Harold Schellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1(4):537--559, 1991.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Model theory

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic; Proof theory

General Terms:
Languages, Theory, Verification

Keywords:
bunched implications, classical bi, completeness, cut-elimination, display logic, resource models, semantics