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

Bunched logics: a uniform approach

Docherty, Simon Robert; (2019) Bunched logics: a uniform approach. Doctoral thesis (Ph.D), UCL (University College London). Green open access

[thumbnail of Simon Docherty - Bunched Logics - A Uniform Approach.pdf]
Preview
Text
Simon Docherty - Bunched Logics - A Uniform Approach.pdf

Download (1MB) | Preview

Abstract

Bunched logics have found themselves to be key tools in modern computer science, in particular through the industrial-level program verification formalism Separation Logic. Despite this—and in contrast to adjacent families of logics like modal and substructural logic—there is a lack of uniform methodology in their study, leaving many evident variants uninvestigated and many open problems unresolved. In this thesis we investigate the family of bunched logics—including previously unexplored intuitionistic variants—through two uniform frameworks. The first is a system of duality theorems that relate the algebraic and Kripke-style interpretations of the logics; the second, a modular framework of tableaux calculi that are sound and complete for both the core logics themselves, as well as many classes of bunched logic model important for applications in program verification and systems modelling. In doing so we are able to resolve a number of open problems in the literature, including soundness and completeness theorems for intuitionistic variants of bunched logics, classes of Separation Logic models and layered graph models; decidability of layered graph logics; a characterisation theorem for the classes of bunched logic model definable by bunched logic formulae; and the failure of Craig interpolation for principal bunched logics. We also extend our duality theorems to the categorical structures suitable for interpreting predicate versions of the logics, in particular hyperdoctrinal structures used frequently in Separation Logic.

Type: Thesis (Doctoral)
Qualification: Ph.D
Title: Bunched logics: a uniform approach
Event: UCL (University College London)
Open access status: An open access version is available from UCL Discovery
Language: English
Additional information: Copyright © The Author 2019. Original content in this thesis is licensed under the terms of the Creative Commons Attribution 4.0 International (CC BY 4.0) Licence (https://creativecommons.org/licenses/by/4.0/). Any third-party copyright material present remains the property of its respective owner(s) and is licensed under its existing terms.
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/10073115
Downloads since deposit
495Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item