article

Bunched Logics Displayed

Author:

James BrotherstonAuthors Info & Claims

Studia Logica, Volume 100, Issue 6

Pages 1223 - 1254

https://doi.org/10.1007/s11225-012-9449-0

Published: 01 December 2012 Publication History

Abstract

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their standard presentations. We show how to constrain applications of display-equivalence in our calculi in such a way that an exhaustive proof search need be only finitely branching, and establish a full deduction theorem for the bunched logics with classical additives, BBI and CBI. We also show that the standard sequent calculus for BI can be seen as a reformulation of its display calculus, and argue that analogous sequent calculi for the other varieties of bunched logic are very unlikely to exist.

References

[1]

ABRAMSKY, SAMSON, and JOUKO VÄÄNÄNEN, From IF to BI; a tale of dependence and separation, Synthese 167(2):207-230, 2009.

[2]

BELNAP, Jr., NUEL D., Display logic, Journal of Philosophical Logic 11:375-417, 1982.

[3]

BERDINE, JOSH, and PETER O'HEARn, Strong update, disposal and encapsulation in bunched typing, in Proceedings of MFPS-22, vol. 158 of ENTCS, Elsevier B.V., 2006, pp. 81-98.

[4]

BROTHERSTON, JAMES, A unified display proof theory for bunched logic, in Proceedings of MFPS-26, vol. 265 of ENTCS, Elsevier B.V., 2010, pp. 197-211.

[5]

BROTHERSTON, JAMES, and CRISTIANO CALCAGNO, Classical BI (A logic for reasoning about dualising resource), in Proceedings of POPL-36, ACM, 2009, pp. 328-339.

[6]

BROTHERSTON, JAMES, and CRISTIANO CALCAGNO, Classical BI: Its semantics and proof theory, Logical Methods in Computer Science 6:3, 2010.

[7]

BROTHERSTON, JAMES, and MAX KANOVICH, Undecidability of propositional separation logic and its neighbours, in Proceedings of LICS-25, IEEE Computer Society, 2010, pp. 137-146.

[8]

BRÜNNLER, Kai, Deep inference and its normal form of derivations, in Proceedings of CiE, vol. 3988 of LNCS, 2006, pp. 65-74.

[9]

CALCAGNO, CRISTIANO, PHILIPPA GARDNER, and URI ZARFATY, Context logic as modal logic: Completeness and parametric inexpressivity, in Proceedings of POPL- 34, ACM, 2007, pp. 123-134.

[10]

CHANG, BOR-YUH EVAN, and XAVIER RIVAL, Relational inductive shape analysis, in Proceedings of POPL-35, ACM, 2008, pp. 247-260.

[11]

CHIN, WEI-NGAN, CRISTINA DAVID, HUU HAI NGUYEN, and SHENGCHAO QIN, Enhancing modular OO verification with separation logic, in Proceedings of POPL-35, ACM, 2008, pp. 87-99.

[12]

COLLINSON, MATTHEW, DAVID PYM, and EDMUND ROBINSON, Bunched polymorphism, Mathematical Structures in Computer Science 18(6):1091-1132, 2008.

Digital Library

[13]

DISTEFANO, DINO, and MATTHEW PARKINSON, jStar: Towards practical verification for Java, in Proceedings of OOPSLA, ACM, 2008, pp. 213-226.

[14]

GALMICHE, DIDIER, and DOMINIQUE LARCHEY-WENDLING, Expressivity properties of Boolean BI through relational models, in Proceedings of FSTTCS, vol. 4337 of LNCS, Springer, 2006, pp. 357-368.

[15]

GALMICHE, DIDIER, DANIEL MÉRY, and DAVID PYM, The semantics of BI and resource tableaux, Mathematical Structures in Computer Science 15:1033-1088, 2005.

Digital Library

[16]

GORÉ, RAJEEV, Gaggles, Gentzen and Galois: How to display your favourite substructural logic, Logic Journal of the IGPL 6(5):669-694, 1998.

[17]

ISHTIAQ, SAMIN, and PETER W. O'HEARN, BI as an assertion language for mutable data structures, in Proceedings of POPL-28, ACM, 2001, pp. 14-26.

[18]

KRACHT, MARCUS, Power and weakness of the modal display calculus, in Heinrich Wansing, (ed.), Proof Theory of Modal Logic, Kluwer, 1996, pp. 93-121.

[19]

LARCHEY-WENDLING, DOMINIQUE, and DIDIER GALMICHE, Exploring the relation between intuitionistic BI and Boolean BI: An unexpected embedding, Mathematical Structures in Computer Science 19:1-66, 2009.

[20]

LARCHEY-WENDLING, DOMINIQUE, and DIDIER GALMICHE, The undecidability of Boolean BI through phase semantics, in Proceedings of LICS-25, IEEE Computer Society, 2010, pp. 140-149.

[21]

LINCOLN, PATRICK, JOHN C. MITCHELL, ANDRE SCEDROV, and NATARAJAN SHANKAR, Decision problems for propositional linear logic, Annals of Pure and Applied Logic 56(1-3):239-311, 1992.

[22]

O'HEARN, PETER W., and DAVID J. PYM, The logic of bunched implications, Bulletin of Symbolic Logic 5(2):215-244, 1999.

[23]

PYM, DAVID, The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series, Kluwer, 2002. Errata and remarks (Pym 2008) maintained at http://www.abdn.ac.uk/~csc335/BI-monograph-errata.pdf.

[24]

PYM, DAVID, PETER O'HEARN, and HONGSEOK YANG, Possible worlds and resources: The semantics of BI, Theoretical Computer Science 315(1):257-305, 2004.

Digital Library

[25]

READ, STEPHEN, Relevant Logic: A Philosophical Examination, Basil Blackwell, 1987.

[26]

REED, JASON, A Hybrid Logical Framework, Ph.D. thesis, Carnegie Mellon University, 2009.

[27]

RESTALL, GREG, Displaying and deciding substructural logics 1: Logics with contraposition, Journal of Philosophical Logic 27:179-216, 1998.

[28]

REYNOLDS, JOHN C., Separation logic: A logic for shared mutable data structures, in Proceedings of LICS-17, IEEE Computer Society, 2002, pp. 55-74.

[29]

WANSING, HEINRICH, Constructive negation, implication, and co-implication, Journal of Applied Non-Classical Logics 18(2-3):341-364, 2008.

Cited By

Frumin DD’Osualdo Evan den Heuvel BPérez J(2022)A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrencyProceedings of the ACM on Programming Languages10.1145/35633186:OOPSLA2(841-869)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563318
Frumin DPopescu AZdancewic S(2022)Semantic cut elimination for the logic of bunched implications, formalized in CoqProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503690(291-306)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503690
Pym D(2019)Resource semanticsACM SIGLOG News10.1145/3326938.33269406:2(5-41)Online publication date: 22-Apr-2019
https://dl.acm.org/doi/10.1145/3326938.3326940
Show More Cited By

Index Terms

Bunched Logics Displayed

Index terms have been assigned to the content through auto-classification.

Recommendations

A Unified Display Proof Theory for Bunched Logic

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their ...
A Paraconsistent Linear-time Temporal Logic

Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time ...
Semantical Analysis of the Logic of Bunched Implications
Abstract
We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Studia Logica

Studia Logica Volume 100, Issue 6

December 2012

252 pages

ISSN:0039-3215

Issue’s Table of Contents

Copyright © Copyright © 2012 Springer Science+Business Media Dordrecht.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 December 2012

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Frumin DD’Osualdo Evan den Heuvel BPérez J(2022)A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrencyProceedings of the ACM on Programming Languages10.1145/35633186:OOPSLA2(841-869)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563318
Frumin DPopescu AZdancewic S(2022)Semantic cut elimination for the logic of bunched implications, formalized in CoqProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503690(291-306)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503690
Pym D(2019)Resource semanticsACM SIGLOG News10.1145/3326938.33269406:2(5-41)Online publication date: 22-Apr-2019
https://dl.acm.org/doi/10.1145/3326938.3326940
Ciabattoni ARamanayake R(2016)Power and Limits of Structural Display RulesACM Transactions on Computational Logic10.1145/287477517:3(1-39)Online publication date: 17-Feb-2016
https://dl.acm.org/doi/10.1145/2874775
Brotherston JKanovich M(2014)Undecidability of Propositional Separation Logic and Its NeighboursJournal of the ACM10.1145/254266761:2(1-43)Online publication date: 24-Apr-2014
https://dl.acm.org/doi/10.1145/2542667
Ciabattoni ARamanayake RWansing H(2014)Hypersequent and Display Calculi --- a Unified PerspectiveStudia Logica10.1007/s11225-014-9566-z102:6(1245-1294)Online publication date: 1-Dec-2014
https://dl.acm.org/doi/10.1007/s11225-014-9566-z
Ciabattoni ARamanayake R(2013)Structural Extensions of Display CalculiProceedings of the 20th International Workshop on Logic, Language, Information, and Computation - Volume 807110.1007/978-3-642-39992-3_10(81-95)Online publication date: 20-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-642-39992-3_10

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents