Print Email Facebook Twitter Iris from the ground up Title Iris from the ground up: A modular foundation for higher-order concurrent separation logic Author Jung, Ralf (Max Planck Institute for Software Systems (MPI-SWS)) Krebbers, R.J. (TU Delft Programming Languages) Jourdan, Jacques-Henri (Max Planck Institute for Software Systems (MPI-SWS)) Bizjak, Aleš (Aarhus University) Birkedal, Lars (Aarhus University) Dreyer, Derek (Max Planck Institute for Software Systems (MPI-SWS)) Date 2018 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. To reference this document use: http://resolver.tudelft.nl/uuid:3b9def46-2d97-4ed8-aa27-dcb8698ed6f2 DOI https://doi.org/10.1017/S0956796818000151 Embargo date 2019-05-01 ISSN 0956-7968 Source Journal of Functional Programming, 28, 1-73 Bibliographical note Accepted Author Manuscript Part of collection Institutional Repository Document type journal article Rights © 2018 Ralf Jung, R.J. Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer Files PDF 47928962_paper.pdf 818.13 KB Close viewer /islandora/object/uuid:3b9def46-2d97-4ed8-aa27-dcb8698ed6f2/datastream/OBJ/view