Iris Project

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

Coq Formalization Tutorial Material Formal Documentation (v3.1) Mailing List Chat

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.

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

Publications

Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages, Lissabon, Portugal
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer
Journal of Functional Programming (JFP), Volume 28, e20, November 2018
This is a significantly revised and expanded synthesis of the Iris 2.0 and 3.0 papers.
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
In ICFP 2018: ACM SIGPLAN International Conference on Functional Programming, St. Louis, Missouri, United States
Mtac2: Typed Tactics for Backward Reasoning in Coq
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
In ICFP 2018: ACM SIGPLAN International Conference on Functional Programming, St. Louis, Missouri, United States
Section 5 contains a case study using the Iris Proof Mode.
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
Dan Frumin, Robbert Krebbers, Lars Birkedal
In LICS 2018: ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
In POPL 2018: ACM SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, CA
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
In POPL 2018: ACM SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, CA
On Models of Higher-Order Separation Logic
Aleš Bizjak, Lars Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics, Ljubljana, Slovenia
Robust and Compositional Verification of Object Capability Patterns
David Swasey, Deepak Garg, Derek Dreyer
In OOPSLA 2017: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
Recipient of OOPSLA 2017 Distinguished Paper Award
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis
In ECOOP 2017: European Conference on Object-Oriented Programming, Barcelona, Spain
Recipient of ECOOP 2017 Distinguished Paper Award
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti, Ralf Jung, Robert Harper
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, Lars Birkedal
In ESOP 2017: European Symposium on Programming, Uppsala, Sweden
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany, Lars Birkedal
In POPL 2017: ACM SIGPLAN 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, Lars Birkedal
In POPL 2017: ACM SIGPLAN Symposium on Principles of Programming Languages, Paris, France
Higher-Order Ghost State ("Iris 2.0")
Ralf Jung, Robbert Krebbers, Lars Birkedal, 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, Derek Dreyer
In POPL 2015: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India

Draft papers

Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Lars Birkedal
Submitted for publication
Mechanized Relational Verification of Concurrent Programs with Continuations
Amin Timany, Lars Birkedal
Submitted for publication

Case studies, MSc theses, Abstracts, Talks

Verifying a Concurrent Data-Structure from the Dartino Framework
Morten Krogh-Jespersen, Thomas Dinsdale-Young, and Lars Birkedal
Formalizing Concurrent Stacks With Helping: A Case Study In Iris
Daniel Gratzer, Mathias Høier, Aleš Bizjak, and Lars Birkedal
Verifying Hash Tables in Iris
Esben Glavind Clausen
Master's thesis at Aarhus University supervised by Lars Birkedal, June 2017
Logical Relations in Iris
Amin Timany, Robbert Krebbers, Lars Birkedal
At CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Paris, France
Unifying Worlds and Resources
Ralf Jung, 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
KU Leuven

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)