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

Why Separation Logic Works

Pym, D; Spring, J; O'Hearn, P; (2019) Why Separation Logic Works. Philosophy and Technology , 32 pp. 483-516. 10.1007/s13347-018-0312-8. Green open access

[thumbnail of Pym2018_Article_WhySeparationLogicWorks.pdf]
Preview
Text
Pym2018_Article_WhySeparationLogicWorks.pdf - Published Version

Download (834kB) | Preview

Abstract

One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer’s conceptual model of a program’s manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to (a subset of) the problems, process, and results of computer scientists for those outside the field.

Type: Article
Title: Why Separation Logic Works
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/s13347-018-0312-8
Publisher version: https://doi.org/10.1007/s13347-018-0312-8
Language: English
Additional information: © The Author(s) 2018. Open Access: This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
Keywords: Separation Logic, Programming and verification, Logical modelling, Modelling strategies, Software engineering, Philosophy of engineering
UCL classification: UCL
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/10048925
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item