UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

A Stone-type Duality Theorem for Separation Logic Via its Underlying Bunched Logics

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. Green open access

[img]
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
Downloads since deposit
54Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item