A Higher-Order Concurrent Separation Logic Framework,
implemented and verified in the Coq
proof assistant
Coq Formalization Technical Reference (v4.2) Mailing List Chat
Learning Iris Events Publications PhD dissertations Other material
Iris is a framework that can be used for reasoning about safety of concurrent programs, as the logic in logical relations, to reason about type-systems, data-abstraction etc. In case of questions, please contact us on the Iris Club list or in our chat room.
Some useful resources designed to learn Iris and its Coq implementation:
A selection of papers that are suited to get started with Iris:
Below, we give an overview of the research that uses Iris one way or another.
Case studies, MSc theses, abstracts, talks:
The Iris project has been supported by the following grants:
Grants from The Danish Council for Independent Research, Sapere Aude: DFF–Advanced Grant 2013 (more information)
2015 ERC Consolidator Grant (more information)
Villum Investigator grant (no. 25804) from The Villum Foundation from 2019-2025. (more information)