Iris from the ground up

A modular foundation for higher-order concurrent separation logic

Journal article (2018)

Authors

Ralf Jung Max Planck Institute for Software Systems (MPI-SWS)
R.J. Krebbers Programming Languages - EEMCS
Jacques-Henri Jourdan Max Planck Institute for Software Systems (MPI-SWS)
Aleš Bizjak Aarhus University
Lars Birkedal Aarhus University
Derek Dreyer Max Planck Institute for Software Systems (MPI-SWS)
Research Group
Programming Languages (EEMCS) (TU Delft)
Copyright: © 2018 Ralf Jung, R.J. Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer
DOI: https://doi.org/10.1017/S0956796818000151
More Info
expand_more

Published Date

2018

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

Research Group

Programming Languages

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.

Files

47928962_paper.pdf
(pdf | 0.799 Mb)
- Embargo expired in 01-05-2019