Stone-Type Dualities for Separation Logics
Stone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because -- in addition to elegant abstraction -- they strengthen soundness and completeness to a categorical equivalence, yielding a framework through which both algebraic and topologi...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/3984/pdf |
| _version_ | 1827322790629343232 |
|---|---|
| author | Simon Docherty David Pym |
| author_facet | Simon Docherty David Pym |
| author_sort | Simon Docherty |
| collection | DOAJ |
| description | Stone-type duality theorems, which relate algebraic and
relational/topological models, are important tools in logic because -- in
addition to elegant abstraction -- they strengthen soundness and completeness
to a categorical equivalence, yielding a framework through which both algebraic
and topological methods can be brought to bear on a logic. We give a systematic
treatment of Stone-type duality for the structures that interpret bunched
logics, starting with the weakest systems, recovering the familiar BI and
Boolean BI (BBI), and extending to both classical and intuitionistic Separation
Logic. We demonstrate the uniformity and modularity of this analysis by
additionally capturing the bunched logics obtained by extending BI and BBI with
modalities and multiplicative connectives corresponding to disjunction,
negation and falsum. This includes the logic of separating modalities (LSM), De
Morgan BI (DMBI), Classical BI (CBI), and the sub-classical family of logics
extending Bi-intuitionistic (B)BI (Bi(B)BI). We additionally obtain as
corollaries soundness and completeness theorems for the specific Kripke-style
models of these logics as presented in the literature: for DMBI, the
sub-classical logics extending BiBI and a new bunched logic, Concurrent Kleene
BI (connecting our work to Concurrent Separation Logic), this is the first time
soundness and completeness theorems have been proved. We thus obtain a
comprehensive semantic account of the multiplicative variants of all standard
propositional connectives in the bunched logic setting. This approach
synthesises a variety of techniques from modal, substructural and categorical
logic and contextualizes the "resource semantics" interpretation underpinning
Separation Logic amongst them. |
| first_indexed | 2024-04-25T01:34:30Z |
| format | Article |
| id | doaj.art-6d31459f5aa94a5da35fe820bc84bafd |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:30Z |
| publishDate | 2019-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-6d31459f5aa94a5da35fe820bc84bafd2024-03-08T10:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-03-01Volume 15, Issue 110.23638/LMCS-15(1:27)20193984Stone-Type Dualities for Separation LogicsSimon DochertyDavid PymStone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because -- in addition to elegant abstraction -- they strengthen soundness and completeness to a categorical equivalence, yielding a framework through which both algebraic and topological methods can be brought to bear on a logic. We give a systematic treatment of Stone-type duality for the structures that interpret bunched logics, starting with the weakest systems, recovering the familiar BI and Boolean BI (BBI), and extending to both classical and intuitionistic Separation Logic. We demonstrate the uniformity and modularity of this analysis by additionally capturing the bunched logics obtained by extending BI and BBI with modalities and multiplicative connectives corresponding to disjunction, negation and falsum. This includes the logic of separating modalities (LSM), De Morgan BI (DMBI), Classical BI (CBI), and the sub-classical family of logics extending Bi-intuitionistic (B)BI (Bi(B)BI). We additionally obtain as corollaries soundness and completeness theorems for the specific Kripke-style models of these logics as presented in the literature: for DMBI, the sub-classical logics extending BiBI and a new bunched logic, Concurrent Kleene BI (connecting our work to Concurrent Separation Logic), this is the first time soundness and completeness theorems have been proved. We thus obtain a comprehensive semantic account of the multiplicative variants of all standard propositional connectives in the bunched logic setting. This approach synthesises a variety of techniques from modal, substructural and categorical logic and contextualizes the "resource semantics" interpretation underpinning Separation Logic amongst them.https://lmcs.episciences.org/3984/pdfcomputer science - logic in computer science03b70f.3.1f.3.2f.4.1 |
| spellingShingle | Simon Docherty David Pym Stone-Type Dualities for Separation Logics Logical Methods in Computer Science computer science - logic in computer science 03b70 f.3.1 f.3.2 f.4.1 |
| title | Stone-Type Dualities for Separation Logics |
| title_full | Stone-Type Dualities for Separation Logics |
| title_fullStr | Stone-Type Dualities for Separation Logics |
| title_full_unstemmed | Stone-Type Dualities for Separation Logics |
| title_short | Stone-Type Dualities for Separation Logics |
| title_sort | stone type dualities for separation logics |
| topic | computer science - logic in computer science 03b70 f.3.1 f.3.2 f.4.1 |
| url | https://lmcs.episciences.org/3984/pdf |
| work_keys_str_mv | AT simondocherty stonetypedualitiesforseparationlogics AT davidpym stonetypedualitiesforseparationlogics |