Separation logic for sequential programs (functional pearl)
The work
| Title | Separation logic for sequential programs (functional pearl) |
|---|---|
| Authors | Arthur Charguéraud |
| Type | article |
| Year | 2020 |
| Citekey | chargueraud2020separation |
Where it appeared
| Published in | Proceedings of the ACM on Programming Languages |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 4 |
| Issue | ICFP |
| Pages | 116:1--116:43 |
Identifiers
| DOI | 10.1145/3408998 |
|---|---|
| OpenAlex | W3047334575 |
Access
| Landing page | https://doi.org/10.1145/3408998 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/3408998 |
Abstract
This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancements. The formalization serves as support for a course that follows the style of the successful Software Foundations series, with all the statement and proofs formalized in Coq. This course only assumes basic knowledge of lambda-calculus, semantics and logics, and therefore should be accessible to a broad audience.
Copy held
| Kind | PDF, 1.1 MB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Opens at | page 2 |
| Where it came from | https://inria.hal.science/hal-03108936/file/seq_seplogic.pdf |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-21 |
Cite it as
@article{chargueraud2020separation,
title = {Separation logic for sequential programs (functional pearl)},
author = {Arthur Charguéraud},
year = {2020},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
pages = {116:1--116:43},
publisher = {Association for Computing Machinery},
doi = {10.1145/3408998},
url = {https://dl.acm.org/doi/pdf/10.1145/3408998},
}
This record lives at https://refs.drheap.org/chargueraud2020separation/ and will keep doing so.