Bunched logics displayed

DOI10.1007/s11225-012-9449-0zbMath1282.03011MaRDI QIDQ1935559

James Brotherston

Publication date: 18 February 2013

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-012-9449-0

zbMATH Keywords

cut elimination; proof theory; bunched logic; display calculus

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

Related Items

Separation logics and modalities: a survey, Unnamed Item, Unnamed Item, Power and Limits of Structural Display Rules, Semantical analysis of the logic of bunched implications, A stone-type duality theorem for separation logic via its underlying bunched logics, Hypersequent and display calculi -- a unified perspective, Unnamed Item, Undecidability of Propositional Separation Logic and Its Neighbours

Uses Software

• jStar

Cites Work

• Unnamed Item
• Unnamed Item
• From IF to BI. A tale of dependence and separation
• Decision problems for propositional linear logic
• Displaying and deciding substructural logics. I: Logics with contraposition
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Display logic
• The semantics and proof theory of the logic of bunched implications
• A Unified Display Proof Theory for Bunched Logic
• Undecidability of Propositional Separation Logic and Its Neighbours
• Context logic as modal logic
• Enhancing modular OO verification with separation logic
• Relational inductive shape analysis
• The semantics of BI and resource tableaux
• Bunched polymorphism
• Classical BI: Its Semantics and Proof Theory
• Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
• Constructive negation, implication, and co-implication
• Gaggles, Gentzen and Galois: how to display your favourite substructural logic
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• Classical BI
• Expressivity Properties of Boolean BI Through Relational Models
• Logical Approaches to Computational Barriers