Iris Project

Iris is a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.

Coq Formalization Formal Documentation Mailing List

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.

Below, we give an overview of the research that uses Iris one way or another.

Papers

A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti, Ralf Jung and Robert Harper
To appear in ESOP 2017: European Symposium on Programming, Uppsala, Sweden
The Essence of Higher-Order Concurrent Separation Logic ("Iris 3.0")
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer and Lars Birkedal
To appear in ESOP 2017: European Symposium on Programming, Uppsala, Sweden
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany and Lars Birkedal
In POPL 2017: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Morten Krogh-Jespersen, Kasper Svendsen and Lars Birkedal
In POPL 2017: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France
Higher-Order Ghost State ("Iris 2.0")
Ralf Jung, Robbert Krebbers, Lars Birkedal and Derek Dreyer
In ICFP 2016: ACM SIGPLAN International Conference on Functional Programming, Nara, Japan
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning ("Iris 1.0")
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal and Derek Dreyer
In POPL 2015: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India

Workshop submissions

Logical Relations in Iris
Amin Timany, Robbert Krebbers and Lars Birkedal
At CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Paris, France
Unifying Worlds and Resources
Ralf Jung and Derek Dreyer
At HOPE 2015: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Vancouver, Canada

Main research groups involved

Aarhus University
Max Planck Institute for Software Systems
Delft University of Technology

Grants

The Iris project has been supported by the following grants:

ModuRes

Modular Reasoning about Concurrent Higher-Order Imperative Programs
Card image

Grants from The Danish Council for Independent Research, Sapere Aude: DFF–Advanced Grant 2013 (more Information)

RustBelt

Logical Foundations for the Future of Safe Systems Programming
Card image

2015 ERC Consolidator Grant (more information)