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

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.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as JSONXMLCSV

Downloads by country - last 12 months

Export as XMLCSVJSON

Archive Staff Only

View Item