Separation logic and abstraction
The work
| Authors | Matthew Parkinson; Gavin M. Bierman |
|---|---|
| Editors | |
| Type | article |
| Year | 2005 |
| Citekey | parkinson2005separation |
Where it appeared
| Published in | ACM SIGPLAN Notices |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 40 |
| Issue | 1 |
| Pages | 247--258 |
Identifiers
| DOI | 10.1145/1047659.1040326 |
|---|---|
| OpenAlex | W3006137651 |
Access
| Landing page | https://doi.org/10.1145/1047659.1040326 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
In this paper we address the problem of writing specifications for programs that use various forms of modularity, including procedures and Java-like classes. We build on the formalism of separation logic and introduce the new notion of an abstract predicate and, more generally, abstract predicate families. This provides a flexible mechanism for reasoning about the different forms of abstraction found in modern programming languages, such as abstract datatypes and objects. As well as demonstrating the soundness of our proof system, we illustrate its utility with a series of examples.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 14:27 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{parkinson2005separation,
title = {Separation logic and abstraction},
author = {Matthew Parkinson and Gavin M. Bierman},
year = {2005},
journal = {ACM SIGPLAN Notices},
publisher = {Association for Computing Machinery},
volume = {40},
number = {1},
pages = {247--258},
doi = {10.1145/1047659.1040326},
}
This record lives at https://refs.drheap.org/parkinson2005separation/ and will keep doing so.