Iris from the ground up: A modular foundation for higher-order concurrent separation logic
The work
| Title | Iris from the ground up: A modular foundation for higher-order concurrent separation logic |
|---|---|
| Authors | Ralf Jung; Robbert Krebbers; Jacques-Henri Jourdan; Aleš Bizjak; Lars Birkedal; Derek Dreyer |
| Type | article |
| Year | 2018 |
| Citekey | jung2018iris |
Where it appeared
| Published in | Journal of Functional Programming |
|---|---|
| Publisher | Cambridge University Press |
| Volume | 28 |
| Pages | e20 |
Identifiers
| DOI | 10.1017/s0956796818000151 |
|---|
Abstract
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
Copy held
| Kind | PDF, 766.4 kB |
|---|---|
| Retrieved | 2026-08-05 |
| Held | local, for personal reference |
Where this came from
| How it got here | the agent went looking · found via openaire |
|---|---|
| First seen | 2026-08-05 |
| Standing | endorsed |
| Approved | 2026-08-07 |
Cite it as
@article{jung2018iris,
title = {Iris from the ground up: A modular foundation for higher-order concurrent separation logic},
author = {Ralf Jung and Robbert Krebbers and Jacques-Henri Jourdan and Aleš Bizjak and Lars Birkedal and Derek Dreyer},
year = {2018},
journal = {Journal of Functional Programming},
volume = {28},
pages = {e20},
publisher = {Cambridge University Press},
doi = {10.1017/s0956796818000151},
}
This record lives at https://refs.drheap.org/jung2018iris/ and will keep doing so.