Stone-type dualities for separation logics

MaRDI QIDQ3121529zbMATH OpenFDO

Authors Simon Docherty, David Pym

Publication date 18 March 2019

Full work available at URL https://arxiv.org/abs/1710.03021

zbMATH Keywords

algebraic logicbunched logicconcurrent Kleene algebracorrespondence theoryhyperdoctrineKripke semanticsmodal logicnon-classical logicpredicate logicprogram logicseparation logicStone-type dualitysubstructural logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70) Other algebras related to logic (03G25) Lattices and duality (06D50) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Foundations of Software Science and Computational Structures
• Duality in logic and computation (invited paper)
• Dualities for algebras of Fitting's many-valued modal logics
• A modal separation logic for resource dynamics
• Sub-classical Boolean Bunched Logics and the Meaning of Par

Cites work

• A calculus and logic of bunched resources and processes
• A logic of separating modalities
• A modal BI logic for dynamic resource properties
• A modal separation logic for resource dynamics
• A new proof of Sahlqvist's theorem on modal definability and completeness
• A program construction and verification tool for separation logic
• A semantics for concurrent separation logic
• A substructural logic for layered graphs
• Algebra and logic for resource-based systems modelling
• Algebraic methods in philosophical logic
• Algebraic separation logic
• BI as an assertion language for mutable data structures
• Boolean Algebras with Operators. Part I
• Bunched logics displayed
• Bunched polymorphism
• Classical BI: Its Semantics and Proof Theory
• Coalgebraic semantics of modal logics: an overview
• Completeness via canonicity for distributive substructural logics: a coalgebraic perspective
• Compositional shape analysis by means of bi-abduction
• Context logic as modal logic, completeness and parametric inexpressivity
• Dijkstra and Hoare monads in monadic computation
• Duality for algebras of relevant logics
• Exemplaric Expressivity of Modal Logics
• Expressivity Properties of Boolean BI Through Relational Models
• Generalising canonical extension to the categorical setting
• Generalized Galois logics. Relational semantics of nonclassical logical calculi
• Healthiness from Duality
• scientific article; zbMATH DE number 3940199 (Why is no real title available?)
• scientific article; zbMATH DE number 3499717 (Why is no real title available?)
• scientific article; zbMATH DE number 1215472 (Why is no real title available?)
• scientific article; zbMATH DE number 549966 (Why is no real title available?)
• scientific article; zbMATH DE number 596497 (Why is no real title available?)
• scientific article; zbMATH DE number 1028833 (Why is no real title available?)
• scientific article; zbMATH DE number 6970800 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1406803 (Why is no real title available?)
• scientific article; zbMATH DE number 6302891 (Why is no real title available?)
• scientific article; zbMATH DE number 2208113 (Why is no real title available?)
• Intuitionistic layered graph logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Layered graph logic as an assertion language for access control policy models
• Looking at separation algebras with Boolean BI-eyes
• Modular tableaux calculi for separation theories
• On Sahlqvist theory for hybrid logics
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Parametric completeness for separation theories
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• Sub-classical Boolean Bunched Logics and the Meaning of Par
• The equational theory of pomsets
• The formal strong completeness of partial monoidal Boolean BI
• The Logic of Bunched Implications
• The semantics of BI and resource tableaux
• Undecidability of propositional separation logic and its neighbours
• Varieties of complex algebras

Cited in

(4)

• A stone-type duality theorem for separation logic via its underlying bunched logics
• scientific article; zbMATH DE number 3893196 (Why is no real title available?)
• Semantical analysis of the logic of bunched implications
• An algebraic glimpse at bunched implications and separation logic

This page was built for publication: Stone-type dualities for separation logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3121529)