TY - JOUR
T1 - Iris from the ground up
T2 - A modular foundation for higher-order concurrent separation logic
AU - Jung, Ralf
AU - Krebbers, Robbert
AU - Jourdan, Jacques-Henri
AU - Bizjak, Aleš
AU - Birkedal, Lars
AU - Dreyer, Derek
N1 - Accepted Author Manuscript
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
U2 - 10.1017/S0956796818000151
DO - 10.1017/S0956796818000151
M3 - Article
SN - 0956-7968
VL - 28
SP - 1
EP - 73
JO - Journal of Functional Programming
JF - Journal of Functional Programming
M1 - e20
ER -