Docherty, S;
Pym, D;
(2018)
A Stone-type Duality Theorem for Separation Logic Via its Underlying Bunched Logics.
Electronic Notes in Theoretical Computer Science
, 336
pp. 101-118.
10.1016/j.entcs.2018.03.018.
Preview |
Text
1-s2.0-S1571066118300215-main.pdf - Published Version Download (346kB) | Preview |
Abstract
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 theorems for the structures that interpret bunched logics, starting with the weakest systems, recovering the familiar Boolean BI, and concluding with Separation Logic. Our results encompass all the known existing algebraic approaches to Separation Logic and prove them sound with respect to the standard store-heap semantics. We additionally recover soundness and completeness theorems of the specific truth-functional models of these logics as presented in the literature. This approach synthesises a variety of techniques from modal, substructural and categorical logic and contextualises the ‘resource semantics’ interpretation underpinning Separation Logic amongst them. As a consequence, theory from those fields — as well as algebraic and topological methods — can be applied to both Separation Logic and the systems of bunched logics it is built upon. Conversely, the notion of indexed resource frame (generalizing the standard model of Separation Logic) and its associated completeness proof can easily be adapted to other non-classical predicate logics.
| Type: | Article |
|---|---|
| Title: | A Stone-type Duality Theorem for Separation Logic Via its Underlying Bunched Logics |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1016/j.entcs.2018.03.018 |
| Publisher version: | https://doi.org/10.1016/j.entcs.2018.03.018 |
| Language: | English |
| Additional information: | This work is licensed under a Creative Commons Attribution 4.0 International License. The images or other third party material in this article are included in the article’s Creative Commons license, unless indicated otherwise in the credit line; if the material is not included under the Creative Commons license, users will need to obtain permission from the license holder to reproduce the material. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/ |
| Keywords: | Separation logic, bunched logic, substructural logic, program logic, categorical logic, algebraic logic, representation, Stone duality, complex systems, hyperdoctrinerelational semantics, topological semantics, completeness |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10049225 |
Archive Staff Only
 |
View Item |
