A stone-type duality theorem for separation logic via its underlying bunched logics

DOI10.1016/j.entcs.2018.03.018OpenAlexW2799457203WikidataQ113317562 ScholiaQ113317562MaRDI QIDQ2130585

David J. Pym, Simon Docherty

Publication date: 25 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.03.018

zbMATH Keywords

representationcompletenessrelational semanticsalgebraic logiccomplex systemssubstructural logiccategorical logicprogram logicseparation logicbunched logictopological semanticsstone dualityhyperdoctrine

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Semantical analysis of the logic of bunched implications ⋮ A categorical duality for algebras of partial functions ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A logic of separating modalities
• Algebraic separation logic
• Generalising canonical extension to the categorical setting
• A calculus and logic of bunched resources and processes
• Bunched logics displayed
• Varieties of complex algebras
• Intuitionistic Layered Graph Logic
• A substructural logic for layered graphs
• A Program Construction and Verification Tool for Separation Logic
• Undecidability of Propositional Separation Logic and Its Neighbours
• Context logic as modal logic
• Looking at Separation Algebras with Boolean BI-eyes
• The semantics of BI and resource tableaux
• Bunched polymorphism
• Classical BI: Its Semantics and Proof Theory
• Algebra and logic for resource-based systems modelling
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• A Substructural Epistemic Resource Logic
• Programming Languages and Systems
• Sub-classical Boolean Bunched Logics and the Meaning of Par
• Expressivity Properties of Boolean BI Through Relational Models
• Compositional Shape Analysis by Means of Bi-Abduction
• Parametric completeness for separation theories
• The formal strong completeness of partial monoidal Boolean BI
• Boolean Algebras with Operators. Part I

This page was built for publication: A stone-type duality theorem for separation logic via its underlying bunched logics