Iris: A Basis for Concurrent Reasoning

Introduction

Iris is a higher-order impredicative concurrent separation logic with a simple premise: Ghost state and invariants are all you need. Resource algebras, a structured but generic form of ghost state, enable us to express — and invariants enable us to enforce — user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency.

Technical development

The latest version of the technical development are available in the Git repository. This includes a Coq formalization of Iris, a rich body of examples, and a technical appendix covering the base logic and the program logic. The technical appendix is also available in compiled PDF form.

Mailing list

Discussion about Iris happens on the Iris-Club mailing list. This is also the right place to ask in case of trouble with the Coq formalization.

Papers

People