Local Action and Abstract Separation Logic
The work
| Authors | Cristiano Calcagno; Peter W. O'Hearn; Hongseok Yang |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2007 |
| Citekey | calcagno2007localaction |
Where it appeared
| Published in | 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) |
|---|---|
| Publisher | IEEE |
| Pages | 366--378 |
Identifiers
| DOI | 10.1109/lics.2007.30 |
|---|---|
| OpenAlex | W2148687959 |
Access
| Landing page | https://doi.org/10.1109/lics.2007.30 |
|---|
Related
| Distinct from | calcagno2007local |
|---|
Abstract
Separation logic is an extension of Hoare's logic which supports a local way of reasoning about programs that mutate memory. We present a study of the semantic structures lying behind the logic. The core idea is of a local action, a state transformer that mutates the state in a local way. We formulate local actions for a class of models called separation algebras, abstracting from the RAM and other specific concrete models used in work on separation logic. Local actions provide a semantics for a generalized form of (sequential) separation logic. We also show that our conditions on local actions allow a general soundness proof for a separation logic for concurrency, interpreted over arbitrary separation algebras.
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-24 07:30 UTC |
Filed under
Cite it as
@inproceedings{calcagno2007localaction,
title = {Local Action and Abstract Separation Logic},
author = {Cristiano Calcagno and Peter W. O'Hearn and Hongseok Yang},
year = {2007},
booktitle = {22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
publisher = {IEEE},
pages = {366--378},
doi = {10.1109/lics.2007.30},
}
This record lives at https://refs.drheap.org/calcagno2007localaction/ and will keep doing so.