An algebraic glimpse at bunched implications and separation logic
From MaRDI portal
Publication:6201543
DOI10.1007/978-3-030-76920-8_5arXiv1709.07063OpenAlexW2759139027MaRDI QIDQ6201543
Publication date: 25 March 2024
Published in: Outstanding Contributions to Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1709.07063
Cites Work
- Concurrent Kleene algebra with tests and branching automata
- Effect algebras and unsharp quantum logics.
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- Cut elimination and strong separation for substructural logics: an algebraic approach
- The structure of generalized BI-algebras and weakening relation algebras
- Relation algebras
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Residuated lattices. An algebraic glimpse at substructural logics
- Adjunct elimination in context logic for trees
- Implicational (semilinear) logics. I: A new hierarchy
- Complete axiomatizations for XPath fragments
- Distributive full Lambek calculus has the finite model property
- Cylindric algebras. Part II
- An algebraic approach to non-classical logics
- Cut-elimination theorem for relevant logics
- Relation algebras as residuated Boolean algebras
- Completeness results for linear logic on Petri nets
- A coalgebraic view of Heyting duality
- Distributive residuated frames and generalized bunched implication algebras
- Adding involution to residuated structures
- Algebraic aspects of cut elimination
- The finite embeddability property for residuated lattices, pocrims and BCK-algebras.
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Display logic
- Decision problems for distributive lattice-ordered semigroups
- Decidable and undecidable logics with a binary modality
- Duality for algebras of relevant logics
- Hoare logic and auxiliary variables
- On the relation between concurrent separation logic and concurrent Kleene algebra
- The semantics and proof theory of the logic of bunched implications
- Minimal varieties of residuated lattices
- On closed elements in closure algebras
- Some modal aspects of XPath
- A substructural logic for layered graphs
- ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages
- Nondeterministic Phase Semantics and the Undecidability of Boolean BI
- Two-Variable Separation Logic and Its Inner Circle
- Higher-order ghost state
- Dafny: An Automatic Program Verifier for Functional Correctness
- Undecidability of Propositional Separation Logic and Its Neighbours
- Context logic as modal logic
- Featherweight VeriFast
- The semantics of BI and resource tableaux
- Scalable Shape Analysis for Systems Code
- Classical BI: Its Semantics and Proof Theory
- Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
- The undecidability of entailment and relevant implication
- Algebraizable logics
- Free Modular Lattices
- Soundness and Completeness of an Axiom System for Program Verification
- The Logic of Bunched Implications
- Nonrepresentable sequential algebras
- Special issue: abductive logic programming
- Separation logics and modalities: a survey
- Bunched Hypersequent Calculi for Distributive Substructural Logics
- The Undecidability of the Word Problems for Projective Geometries and Modular Lattices
- TQL: a query language for semistructured data based on the ambient logic
- Residuated frames with applications to decidability
- Separation Logic with One Quantified Variable
- Anytime, anywhere
- BI as an assertion language for mutable data structures
- Separation logic and abstraction
- Context logic and tree update
- Programming Languages and Systems
- Expressivity Properties of Boolean BI Through Relational Models
- Compositional Shape Analysis by Means of Bi-Abduction
- Parametric completeness for separation theories
- Concurrent Kleene Algebra with Tests
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Programming Languages and Systems
- An axiomatic basis for computer programming
- On closed categories of functors
- Semantics for relevant logics
- On Hoare logic and Kleene algebra with tests
- Tools and Algorithms for the Construction and Analysis of Systems
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: An algebraic glimpse at bunched implications and separation logic
