Iris logo

A Higher-Order Concurrent Separation Logic Framework,
implemented and verified in the Coq proof assistant

Coq Formalization Technical Documentation (v3.4) 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.

Learning Iris

Some useful resources designed to learn Iris and its Coq implementation:

A selection of papers that are suited to get started with Iris:

Events

Publications

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

Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
Glen Mével, Jacques-Henri Jourdan
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Dan Frumin, Robbert Krebbers, Lars Birkedal
In LMCS 2021: Logical Methods in Computer Science
GhostCell: Separating Permissions from Data in Rust
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
Theorems for Free from Separation Logic Specifications
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
Recipient of ICFP 2021 Distinguished Paper Award
GoJournal: A Verified, Concurrent, Crash-Safe Journaling System
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
In OSDI 2021: USENIX Symposium on Operating System Design and Implementation
RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
In PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
Recipient of PLDI 2021 Distinguished Paper Award
Recipient of PLDI 2021 Distinguished Artifact Award
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
In PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin, Robbert Krebbers, Lars Birkedal
In S&P 2021: IEEE Symposium on Security and Privacy
Safe Systems Programming in Rust
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
In Communications of the ACM (CACM), April 2021
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, Dominique Devriese
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
A Separation Logic for Effect Handlers
Paulo Emílio de Vilhena, François Pottier
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon Friis Vindum, Lars Birkedal
In CPP 2021: ACM SIGPLAN International Conference on Certified Programs and Proofs
Reasoning about Monotonicity in Separation Logic
Amin Timany, Lars Birkedal
In CPP 2021: ACM SIGPLAN International Conference on Certified Programs and Proofs
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson
In CPP 2021: ACM SIGPLAN International Conference on Certified Programs and Proofs
Recipient of CPP 2021 Distinguished Paper Award
Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, François Pottier
In ICFP 2020: ACM SIGPLAN International Conference on Functional Programming
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
In ICFP 2020: ACM SIGPLAN International Conference on Functional Programming
Verifying Concurrent Search Structure Templates
Siddharth Krishna, Nisarg Patel, Dennis Shasha, Thomas Wies
In PLDI 2020: ACM SIGPLAN Conference on Programming Language Design and Implementation
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
In ESOP 2020: European Symposium on Programming
RustBelt Meets Relaxed Memory
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer
In POPL 2020: ACM SIGPLAN Symposium on Principles of Programming Languages
Spy Game: Verifying a Local Generic Solver in Iris
Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
In POPL 2020: ACM SIGPLAN Symposium on Principles of Programming Languages
Actris: Session-Type Based Reasoning in Separation Logic
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
In POPL 2020: ACM SIGPLAN Symposium on Principles of Programming Languages
The Future is Ours: Prophecy Variables in Separation Logic
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
In POPL 2020: ACM SIGPLAN Symposium on Principles of Programming Languages
The High-Level Benefits of Low-Level Sandboxing
Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak
In POPL 2020: ACM SIGPLAN Symposium on Principles of Programming Languages
Verifying Concurrent, Crash-Safe Systems with Perennial
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
In SOSP 2019: ACM Symposium on Operating Systems Principles
Mechanized Relational Verification of Concurrent Programs with Continuations
Amin Timany, Lars Birkedal
In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
Semi-Automated Reasoning About Non-Determinism in C Expressions
Dan Frumin, Léon Gondelman, Robbert Krebbers
In ESOP 2019: European Symposium on Programming
Time Credits and Time Receipts in Iris
Glen Mével, Jacques-Henri Jourdan, François Pottier
In ESOP 2019: European Symposium on Programming
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
A Separation Logic for Concurrent Randomized Programs
Joseph Tassarotti, Robert Harper
In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic ("Iris 3.1")
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
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
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
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
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
On Models of Higher-Order Separation Logic
Aleš Bizjak, Lars Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
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
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
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
Interactive Proofs in Higher-Order Concurrent Separation Logic ("Iris Proof Mode")
Robbert Krebbers, Amin Timany, Lars Birkedal
In POPL 2017: ACM SIGPLAN Symposium on Principles of Programming Languages
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
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
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

PhD dissertations

Sessions and Separation
Jonas Kastberg Hinrichsen
IT University of Copenhagen, March 2021
Concurrent Separation Logics for Safety, Refinement, and Security
Dan Frumin
Radboud University Nijmegen, March 2021
Understanding and Evolving the Rust Programming Language
Ralf Jung
MPI-SWS and Saarbrücken Graduate School of Computer Science, August 2020
Recipient of Honorable Mention for the ACM Doctoral Dissertation Award
Recipient of ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award
Recipient of ETAPS Doctoral Dissertation Award
Recipient of Otto Hahn Medal
Compositional Abstractions for Verifying Concurrent Data Structures
Siddharth Krishna
New York University, September 2019
Verifying Concurrent Randomized Algorithms
Joseph Tassarotti
Carnegie Mellon University, January 2019
Towards Modular Reasoning for Stateful and Concurrent Programs
Morten Krogh-Jespersen
Aarhus University, September 2018
Contributions in Programming Languages Theory
Amin Timany
KU Leuven, May 2018

Other material

Draft papers:

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
Submitted for publication

Case studies, MSc theses, abstracts, talks:

Mechanized Reasoning about a Capability Machine
Aina Linn Georges, Alix Trieu, Lars Birkedal
Extended Abstract for talk at PRISC 2020: Principles of Secure Compilation
Verifying a Concurrent Data-Structure from the Dartino Framework
Morten Krogh-Jespersen, Thomas Dinsdale-Young, Lars Birkedal
Formalizing Concurrent Stacks With Helping: A Case Study In Iris
Daniel Gratzer, Mathias Høier, Aleš Bizjak, 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
Radboud University

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)