A Unified Display Proof Theory for Bunched Logic
From MaRDI portal
Publication:3178253
DOI10.1016/j.entcs.2010.08.012zbMath1343.03018MaRDI QIDQ3178253
Publication date: 8 July 2016
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2010.08.012
03B70: Logic in computer science
03F05: Cut-elimination and normal-form theorems
03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F03: Proof theory in general (including proof-theoretic semantics)
Related Items
Monoidal logics: completeness and classical systems, Proof tactics for assertions in separation logic, Bunched logics displayed, Focused proof-search in the logic of bunched implications, Craig Interpolation in Displayable Logics, Completeness for a First-Order Abstract Separation Logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- 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
- Hybridizing a Logical Framework
- Nondeterministic Phase Semantics and the Undecidability of Boolean BI
- 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
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
- 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
