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 in our chat room.

Learning Iris

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

• The Iris lecture notes provide a tutorial style introduction to Iris, including a number of exercises (but most of it not in Coq).
• The Iris tutorial in Coq is an Software-Foundations-style introduction to Iris, in Coq. It starts from scratch and does not assume knowledge of the Iris Lecture Notes, but many of the examples are drawn from the Iris Lecture Notes.
• The second half of Derek Dreyer's Semantics lecture notes gives an introduction to Iris, including exercises and a Coq development.
• The Iris Tutorial at POPL'21 contains a number of exercises to practice the Iris tactics in Coq. A video recording of the tutorial talk is also available.
• The paper A Logical Approach to Type Soundness shows how Iris can be used to prove type soundness. See also the video recording of Derek Dreyer's POPL'18 keynote and the Iris Tutorial at POPL'20.

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

• The Iris From The Ground Up paper contains an extensive description of the rules and the model of the Iris logic.
• The Iris Proofmode paper (Section 3) contains a brief tutorial to the Iris tactics in Coq.
• The Iris Proof Mode (IPM) / MoSeL and the HeapLang documentation provide a reference of the Iris tactics in Coq.

Events

• 3 June–7 June 2024: The Fourth Iris Workshop, Zürich, Switzerland
• 15 January 2024: Tutorial on Iris and Session Types at POPL, London, UK
• 22 May–26 May 2023: The Third Iris Workshop, Saarbrücken, Germany
• 2 May–6 May 2022: The Second Iris Workshop, Nijmegen, The Netherlands
• 18 January 2021: Tutorial on Iris at POPL, Virtual
• 20 January 2020: Tutorial on Proving Semantic Type Soundness in Iris at POPL, New Orleans, USA
• 28 October–1 November 2019: The First Iris Workshop, Aarhus, Denmark
• 8 January 2018: Tutorial on Iris at POPL, Los Angeles, USA

Publications

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

A Logical Approach to Type Soundness

Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal
Journal of the ACM (JACM), Volume 71, Issue 6, Article No. 40, November 2024

.pdf JACM webpage

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly

Maxime Legoupil, June Rousseau, Aina Linn Georges, Jean Pichon-Pharabod, Lars Birkedal
In OOPSLA 2024: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Artifact

Verified Lock-Free Session Channels with Linking

Thomas Somers, Robbert Krebbers
In OOPSLA 2024: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Artifact

Multris: Functional Verification of Multiparty Message Passing in Separation Logic

Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers
In OOPSLA 2024: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Artifact

Tachis: Higher-Order Separation Logic with Credits for Expected Costs

Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
In OOPSLA 2024: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Artifact Coq development

Snapshottable Stores

Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming
Recipient of ICFP 2024 Distinguished Paper Award

.pdf Coq development

Almost-Sure Termination by Guarded Refinement

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming

.pdf Artifact Coq development

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming
Recipient of ICFP 2024 Distinguished Paper Award

.pdf Artifact Coq development

The Functional Essence of Imperative Binary Search Trees

Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley
In PLDI 2024: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq

Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer
In PLDI 2024: ACM SIGPLAN International Conference on Programming Language Design and Implementation
Recipient of PLDI 2024 Distinguished Artifact Award

.pdf website

RefinedRust: A Type System for High-Assurance Verification of Rust Programs

Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
In PLDI 2024: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf website

A Proof Recipe for Linearizability in Relaxed Memory Separation Logic

Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang
In PLDI 2024: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Coq development Artifact

Unification for Subformula Linking under Quantifiers

Ike Mulder, Robbert Krebbers
In CPP 2024: ACM SIGPLAN International Conference on Certified Programs and Proofs

[preprint] .pdf Artifact

Thunks and Debits in Separation Logic with Time Credits

François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact

An Iris Instance for Verifying CompCert C Programs

William Mansky, Ke Du
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact website

DisLog: A Separation Logic for Disentanglement

Alexandre Moine, Sam Westrick, Stephanie Balzer
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact

The Logical Essence of Well-Bracketed Control Flow

Amin Timany, Armaël Gueneau, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development

The Essence of Generalized Algebraic Data Types

Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Artifact

Modular Denotational Semantics for Effects with Guarded Interaction Trees

Dan Frumin, Amin Timany, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
Recipient of POPL 2024 Distinguished Paper Award

.pdf Coq development Artifact

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Extended version Coq development Artifact

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Extended version Coq development Artifact

An axiomatic basis for computer programming on the relaxed Arm-A architecture: The AxSL logic

Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
Journal of the ACM (JACM), Volume 71, Issue 1, Article No. 3, February 2024

.pdf Coq development publisher's site

Grove: a Separation-Logic Library for Verifying Distributed Systems

Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
In SOSP 2023: ACM Symposium on Operating Systems Principles

.pdf Extended version

Leaf: Modularity for Temporary Sharing in Separation Logic

Travis Hance, Jon Howell, Oded Padon, Bryan Parno
In OOPSLA 2023: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

publisher's site Extended version Coq development

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
In OOPSLA 2023: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Coq development website Artifact

Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic

Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang
In OOPSLA 2023: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Coq development

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory

Simon Friis Vindum, Lars Birkedal
In OOPSLA 2023: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
Recipient of OOPSLA 2023 Distinguished Paper Award

.pdf Coq development Artifact

Proof Automation for Linearizability in Separation Logic

Ike Mulder, Robbert Krebbers
In OOPSLA 2023: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
Recipient of OOPSLA 2023 Distinguished Artifact Award

.pdf Artifact Coq development

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Paulo Emílio de Vilhena, François Pottier
In LMCS 2023: Logical Methods in Computer Science

.pdf Coq development

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal
In ICFP 2023: ACM SIGPLAN International Conference on Functional Programming

.pdf Artifact Coq development website

Dependent Session Protocols in Separation Logic from First Principles

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
In ICFP 2023: ACM SIGPLAN International Conference on Functional Programming

.pdf Artifact Coq development website

Modular Verification of State-Based CRDTs in Separation Logic

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
In ECOOP 2023: European Conference on Object-Oriented Programming

[preprint] .pdf Coq development website

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control

Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
In OSDI 2023: USENIX Symposium on Operating Systems Design and Implementation

.pdf

Fair Operational Semantics

Dongjae Lee, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur
In PLDI 2023: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Website Coq development

CQS: A Formally-Verified Framework for Fair and Abortable Synchronization

Nikita Koval, Dmitry Khalanskiy, Dan Alistarh
In PLDI 2023: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic

Ike Mulder, Łukasz Czajka, Robbert Krebbers
In PLDI 2023: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Artifact Coq development

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating over FF-A

Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal
In PLDI 2023: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Coq development

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

Xiaojia Rao, Aina Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal
In PLDI 2023: ACM SIGPLAN International Conference on Programming Language Design and Implementation

.pdf Coq development Artifact

A Type System for Effect Handlers and Dynamic Labels

Paulo Emílio de Vilhena, François Pottier
In ESOP 2023: European Symposium on Programming

.pdf Coq development

Higher-Order Leak and Deadlock Free Locks

Jules Jacobs, Stephanie Balzer
In POPL 2023: ACM SIGPLAN Symposium on Principles of Programming Languages
Recipient of POPL 2023 Distinguished Paper Award

.pdf Coq development

A High-Level Separation Logic for Heap Space under Garbage Collection

Alexandre Moine, Arthur Charguéraud, François Pottier
In POPL 2023: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact

DimSum: A Decentralized Approach to Multi-language Semantics and Verification

Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
In POPL 2023: ACM SIGPLAN Symposium on Principles of Programming Languages
Recipient of POPL 2023 Distinguished Paper Award

.pdf Website Coq development Artifact

Purity of an ST monad: full abstraction by semantically typed back-translation

Koen Jacobs, Dominique Devriese, Amin Timany
In OOPSLA 2022: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf Coq development

BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs

Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg
In OOPSLA 2022: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

[preprint] .pdf Artifact Website

Modular Verification of Op-Based CRDTs in Separation Logic

Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal
In OOPSLA 2022: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

[preprint] .pdf Coq development website

Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities

Aïna Linn Georges, Alix Trieu, Lars Birkedal
In OOPSLA 2022: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
Recipient of OOPSLA 2022 Distinguished Paper Award

[preprint] .pdf Coq development

Verified Symbolic Execution with Kripke Specification Monads (and No Meta-programming)

Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese
In ICFP 2022: ACM SIGPLAN International Conference on Functional Programming

.pdf Website Coq development Artifact

Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom

Jules Jacobs, Stephanie Balzer, Robbert Krebbers
In ICFP 2022: ACM SIGPLAN International Conference on Functional Programming

.pdf Artifact

Later Credits: Resourceful Reasoning for the Later Modality ("Iris 4.0")

Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
In ICFP 2022: ACM SIGPLAN International Conference on Functional Programming

.pdf Website (with Coq development) Artifact and appendix

Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic

Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer
In PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation

.pdf Coq development website

RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer
In PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation
Recipient of PLDI 2022 Distinguished Paper Award

.pdf Coq development Creusot development artifact errata

Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris

Ike Mulder, Robbert Krebbers, Herman Geuvers
In PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation

.pdf Coq development

Islaris: Verification of Machine Code Against Authoritative ISA Semantics

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
In PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation

.pdf Coq development

A Self-Dual Distillation of Session Types

Jules Jacobs
In ECOOP 2022: European Conference on Object-Oriented Programming

.pdf Coq development

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic

Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
In LMCS 2022: Logical Methods in Computer Science

.pdf Coq development website

Applying Formal Verification to Microkernel IPC at Meta

Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli
In CPP 2022: ACM SIGPLAN International Conference on Certified Programs and Proofs

.pdf

Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library

Simon Friis Vindum, Dan Frumin, Lars Birkedal
In CPP 2022: ACM SIGPLAN International Conference on Certified Programs and Proofs

.pdf Coq development

Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations

Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
In POPL 2022: ACM SIGPLAN Symposium on Principles of Programming Languages
Recipient of POPL 2022 Distinguished Paper Award

.pdf Coq development Artifact and appendix

Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic

Jules Jacobs, Stephanie Balzer, Robbert Krebbers
In POPL 2022: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development

VIP: Verifying Real-World C Idioms with Integer-Pointer Casts

Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
In POPL 2022: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact and appendix Video

A Separation Logic for Heap Space under Garbage Collection

Jean-Marie Madiot, François Pottier
In POPL 2022: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development Artifact

Verifying Concurrent Multicopy Search Structures

Nisarg Patel, Siddharth Krishna, Dennis Shasha, Thomas Wies
In OOPSLA 2021: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications

.pdf

Certifying the synthesis of heap-manipulating programs

Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey
In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming

.pdf

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

.pdf Coq development

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

.pdf website with Rust and Coq development

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

.pdf Coq development video

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

.pdf website Coq development

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

.pdf code Coq development

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

.pdf website Coq development Artifact and appendix

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

.pdf website Coq development

Compositional Non-Interference for Fine-Grained Concurrent Programs

Dan Frumin, Robbert Krebbers, Lars Birkedal
In S&P 2021: IEEE Symposium on Security and Privacy

[preprint] .pdf Coq development

Safe Systems Programming in Rust

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
In Communications of the ACM (CACM), April 2021

.pdf html + video

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

[preprint] .pdf Coq formalization

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

.pdf technical appendix Coq formalization

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

.pdf technical appendix Coq formalization website

Fully Abstract from Static to Gradual

Koen Jacobs, Amin Timany, Dominique Devriese
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq formalization

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

[preprint] .pdf Coq formalization

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

.pdf

Reasoning about Monotonicity in Separation Logic

Amin Timany, Lars Birkedal
In CPP 2021: ACM SIGPLAN International Conference on Certified Programs and Proofs

[amended after publication] .pdf Coq development

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

.pdf Coq development website

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

.pdf Web development

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

.pdf Coq development website

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

.pdf Coq development

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

.pdf technical appendix Coq development website

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

.pdf website

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

.pdf Coq development

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

.pdf Coq development website

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

.pdf website video

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

.pdf Coq development

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

.pdf Coq development

Mechanized Relational Verification of Concurrent Programs with Continuations

Amin Timany, Lars Birkedal
In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming

.pdf Coq development

Specifying I/O using abstract nested hoare triples in separation logic

Willem Penninckx, Amin Timany, Bart Jacobs
In FTfJP '19: Workshop on Formal Techniques for Java-like Programs

.pdf

Semi-Automated Reasoning About Non-Determinism in C Expressions

Dan Frumin, Léon Gondelman, Robbert Krebbers
In ESOP 2019: European Symposium on Programming

.pdf Coq development website slides

Time Credits and Time Receipts in Iris

Glen Mével, Jacques-Henri Jourdan, François Pottier
In ESOP 2019: European Symposium on Programming

.pdf Coq development

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

.pdf Coq development website

A Separation Logic for Concurrent Randomized Programs

Joseph Tassarotti, Robert Harper
In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages

.pdf Coq development

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.
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation

.pdf technical appendix

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

.pdf website

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.

.pdf website

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

.pdf website Coq development slides

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

.pdf website

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

.pdf Coq development

On Models of Higher-Order Separation Logic

Aleš Bizjak, Lars Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics

.pdf

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

[preprint] .pdf [long version] .pdf Coq development Coq development (VM)

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

.pdf website

A Higher-Order Logic for Concurrent Termination-Preserving Refinement

Joseph Tassarotti, Ralf Jung, Robert Harper
In ESOP 2017: European Symposium on Programming

.pdf website arXiv

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
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation

.pdf technical appendix Coq development

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

.pdf

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

.pdf technical appendix

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
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation

.pdf technical appendix (1/2) technical appendix (2/2) Coq development talk on youtube slides

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
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation

.pdf technical appendix (historic) Coq formalization publisher's site slides

PhD dissertations

Verification of Concurrent Search Structures

Nisarg Patel
New York University, September 2024

.pdf

Guarantees by Construction

Jules Jacobs
Radboud University Nijmegen, June 2024

.pdf

Automated and Foundational Verification of Low-Level Programs

Michael Sammler
MPI-SWS and Saarland University, December 2023
Recipient of Runner-Up Prize for the 2024 Informatics Europe Best Dissertation Award
Recipient of 2024 Dr. Eduard Martin Prize (Saarland University)

.pdf

Separation Logic for Concurrency and Persistency

Simon Friis Vindum
Aarhus University, December 2023

.pdf

Syntax and semantics of modal type theory

Daniel Gratzer
Aarhus University, October 2023

.pdf

Conflict-free Replicated Data Types have Abstract Data Types

Abel Nieto
Aarhus University, June 2023

.pdf

Designing and Proving Robust Safety of Efficient Capability Machine Programs

Aina Linn Georges
Aarhus University, June 2023

.pdf

Higher-Order Separation Logic for Distributed Systems and Security

Simon Oddershede Gregersen
Aarhus University, March 2023

.pdf

Proof of Programs with Effect Handlers

Paulo Emílio de Vilhena
Université Paris Cité, December 2022

.pdf

A Mechanized Program Logic for Concurrent Programs with the Weak Memory Model of Multicore OCaml

Glen Mével
Inria and Université Paris Cité, December 2022

.pdf

Verifying a Concurrent, Crash-Safe File System with Sequential Reasoning

Tej Chajed
Massachusetts Institute of Technology, May 2022
Recipient of Honorable Mention for the 2022 ACM SIGOPS Dennis M. Ritchie Thesis Award

.pdf

Sessions and Separation

Jonas Kastberg Hinrichsen
IT University of Copenhagen, March 2021

.pdf

Concurrent Separation Logics for Safety, Refinement, and Security

Dan Frumin
Radboud University Nijmegen, March 2021

.pdf website

Understanding and Evolving the Rust Programming Language

Ralf Jung
MPI-SWS and Saarland University, August 2020
Recipient of Honorable Mention for the 2020 ACM Doctoral Dissertation Award
Recipient of 2021 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award
Recipient of 2021 ETAPS Doctoral Dissertation Award
Recipient of 2021 Otto Hahn Medal (Max Planck Society)
Recipient of 2021 Dr. Eduard Martin Prize (Saarland University)

.pdf website

Compositional Abstractions for Verifying Concurrent Data Structures

Siddharth Krishna
New York University, September 2019

.pdf

Verifying Concurrent Randomized Algorithms

Joseph Tassarotti
Carnegie Mellon University, January 2019

.pdf

Towards Modular Reasoning for Stateful and Concurrent Programs

Morten Krogh-Jespersen
Aarhus University, September 2018

.pdf

Contributions in Programming Languages Theory

Amin Timany
KU Leuven, May 2018

.pdf

Other material

Case studies, MSc theses, abstracts, talks:

Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms

Mathias Pedersen
Master's thesis at Aarhus University supervised by Amin Timany, June 2024

.pdf Coq development

Logical Foundations Of Language Interoperability Between OCaml and C

Johannes Hostert
Master's thesis at Saarland University supervised by Derek Dreyer, July 2023

.pdf

Verifying a Barrier using Iris

Simcha van Collem
Bachelor's thesis at Radboud University Nijmegen supervised by Robbert Krebbers, March 2023

.pdf Coq development

Mechanized Reasoning about a Capability Machine

Aina Linn Georges, Alix Trieu, Lars Birkedal
Extended Abstract for talk at PRISC 2020: Principles of Secure Compilation

.pdf

Verifying a Concurrent Data-Structure from the Dartino Framework

Morten Krogh-Jespersen, Thomas Dinsdale-Young, Lars Birkedal

.pdf Coq development

Formalizing Concurrent Stacks With Helping: A Case Study In Iris

Daniel Gratzer, Mathias Høier, Aleš Bizjak, Lars Birkedal

.pdf Coq development

Verifying Hash Tables in Iris

Esben Glavind Clausen
Master's thesis at Aarhus University supervised by Lars Birkedal, June 2017

.pdf

Logical Relations in Iris

Amin Timany, Robbert Krebbers, Lars Birkedal
At CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Paris, France

abstract Coq development

Unifying Worlds and Resources

Ralf Jung, Derek Dreyer
At HOPE 2015: 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Vancouver, Canada

talk on youtube slides