Local reasoning about data update
The work
| Authors | Cristiano Calcagno; Philippa Gardner; Uri Zarfaty |
|---|---|
| Editors | |
| Type | article |
| Year | 2007 |
| Citekey | calcagno2007local |
Where it appeared
| Published in | Electronic Notes in Theoretical Computer Science |
|---|---|
| Volume | 172 |
| Pages | 133--175 |
Identifiers
| DOI | 10.1016/j.entcs.2007.02.006 |
|---|
Related
| Distinct from | calcagno2007localaction |
|---|
Abstract
We present local Hoare reasoning about data update, introducing Context Logic for analysing structured data. We apply our reasoning to tree update, heap update, and term rewriting. Our reasoning about heap update is exactly analogous to the local Hoare reasoning of Separation Logic. Our reasoning about tree update and term rewriting can only be done with Context Logic.
A copy is held
pdf, 709.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-23 14:13 UTC |
Filed under
Cite it as
@article{calcagno2007local,
title = {Local reasoning about data update},
author = {Cristiano Calcagno and Philippa Gardner and Uri Zarfaty},
year = {2007},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {172},
pages = {133--175},
doi = {10.1016/j.entcs.2007.02.006},
}
This record lives at https://refs.drheap.org/calcagno2007local/ and will keep doing so.