Relational Parametricity and Separation Logic
The work
| Authors | Lars Birkedal; Hongseok Yang |
|---|---|
| Editors | |
| Type | article |
| Year | 2008 |
| Citekey | birkedal2008relational |
Where it appeared
| Published in | Logical Methods in Computer Science |
|---|---|
| Publisher | Centre pour la Communication Scientifique Directe (CCSD) |
| Volume | Volume 4, Issue 2 |
| Article number | 825 |
Identifiers
| DOI | 10.2168/lmcs-4(2:6)2008 |
|---|---|
| ISSN | 1860-5974 |
Access
| Landing page | https://doi.org/10.2168/lmcs-4(2:6)2008 |
|---|
Related
| Supersedes | birkedal2007relational |
|---|
From crossref.
Abstract
Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types. Our interpretation is based on Reynolds’s relational parametricity, and it provides a formal connection between separation logic and data abstraction.
A copy is held
pdf, 305.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-22 23:22 UTC |
| Approved by | a person 2026-10-23 11:27 UTC |
Filed under
Cite it as
@article{birkedal2008relational,
title = {Relational Parametricity and Separation Logic},
author = {Lars Birkedal and Hongseok Yang},
year = {2008},
journal = {Logical Methods in Computer Science},
publisher = {Centre pour la Communication Scientifique Directe (CCSD)},
volume = {Volume 4, Issue 2},
issn = {1860-5974},
articleno = {825},
doi = {10.2168/lmcs-4(2:6)2008},
}
This record lives at https://refs.drheap.org/birkedal2008relational/ and will keep doing so.