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

Resource semantics: logic as a modelling technology

Pym, D; (2019) Resource semantics: logic as a modelling technology. ACM SIGLOG News , 6 (2) pp. 5-41. 10.1145/3326938.3326940. Green open access

[img]
Preview
Text
Pym_Resource semantics. logic as a modelling technology_AAM.pdf - Accepted version

Download (1MB) | Preview

Abstract

The Logic of Bunched Implications (BI) was introduced by O'Hearn and Pym. The original presentation of BI emphasised its role as a system for formal logic (broadly in the tradition of relevant logic) that has some interesting properties, combining a clean proof theory, including a categorical interpretation, with a simple truth-functional semantics. BI quickly found significant applications in program verification and program analysis, chiefly through a specific theory of BI that is commonly known as 'Separation Logic'. We survey the state of work in bunched logics - which, by now, is a quite large family of systems, including modal and epistemic logics and logics for layered graphs - in such a way as to organize the ideas into a coherent (semantic) picture with a strong interpretation in terms of resources. One such picture can be seen as deriving from an interpretation of BI's semantics in terms of resources, and this view provides a basis for a systematic interpretation of the family of bunched logics, including modal, epistemic, layered graph, and process-theoretic variants, in terms of resources. We explain the basic ideas of resource semantics, including comparisons with Linear Logic and ideas from economics and physics. We include discussions of BI's λ-calculus, of Separation Logic, and of an approach to distributed systems modelling based on resource semantics.

Type: Article
Title: Resource semantics: logic as a modelling technology
Open access status: An open access version is available from UCL Discovery
DOI: 10.1145/3326938.3326940
Publisher version: https://dl.acm.org/citation.cfm?id=3326940
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
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/10074293
Downloads since deposit
39Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item