Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers
In CPP 2026: ACM SIGPLAN Conference on Certified Programs and Proofs
| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Mon, 08 Dec 2025 20:56:04 GMT
access-control-allow-origin: *
etag: W/"69373b64-1f69a"
expires: Sun, 28 Dec 2025 06:12:02 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 546F:3FD64F:747F4C:828A11:6950C7DA
accept-ranges: bytes
age: 0
date: Sun, 28 Dec 2025 06:02:02 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210038-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1766901722.393013,VS0,VE210
vary: Accept-Encoding
x-fastly-request-id: 2caec1ab3059fe9ff1e3540b547b0e9135d3db60
content-length: 19816
Iris Project
A Higher-Order Concurrent Separation Logic Framework,
implemented and verified in the Rocq Prover
Rocq Formalization Technical Reference (v4.3) 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 in our chat room.
Some useful resources designed to learn Iris and its Rocq implementation:
- The Iris lecture notes provide a tutorial style introduction to Iris, including a number of exercises (but most of it not in Rocq).
- The Iris tutorial in Rocq is an Software-Foundations-style introduction to Iris, in Rocq. 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 Rocq development.
- The Iris Tutorial at POPL'21 contains a number of exercises to practice the Iris tactics in Rocq. 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 Rocq.
- The Iris Proof Mode (IPM) / MoSeL and the HeapLang documentation provide a reference of the Iris tactics in Rocq.
Events
- 8 June–12 June 2026: The Sixth Iris Workshop, Klosterneuburg/Vienna, Austria
- 2 June–4 June 2025 (plus two extra days): The Fifth Iris Workshop, Paris, France
- 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
Below, we give an overview of the research that uses Iris one way or another.
- Building Blocks for Step-Indexed Program Logics
- All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
-
Alexandre Moine, Sam Westrick, Joseph Tassarotti
In POPL 2026: ACM SIGPLAN Symposium on Principles of Programming Languages - TypeDis: A Type System for Disentanglement
-
Alexandre Moine, Stephanie Balzer, Alex Xu, Sam Westrick
In POPL 2026: ACM SIGPLAN Symposium on Principles of Programming Languages - A Relational Separation Logic for Effect Handlers
- Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic
- Logical Relations for Formally Verified Authenticated Data Structures
-
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
In CCS 2025: ACM SIGSAC Conference on Computer and Communications Security - Formal Semantics and Program Logics for a Fragment of OCaml
-
Remy Seassau, Irene Yoon, Jean-Marie Madiot, François Pottier
In ICFP 2025: ACM SIGPLAN International Conference on Functional Programming - Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
-
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In ICFP 2025: ACM SIGPLAN International Conference on Functional Programming - Reasoning about Weak Isolation Levels in Separation Logic
- Modular, Full-System Verification
-
Gregory Malecha, Hoang-Hai Dang, Paolo G. Giarrusso, Simon Hudon, Jan-Oliver Kaiser, David Swasey
In HotOS 2025: ACM SIGOPS Workshop in Hot Topics in Operating Systems - Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
-
Janggun Lee, Jeonghyeon Kim, Jeehoon Kang
In PLDI 2025: ACM SIGPLAN International Conference on Programming Language Design and Implementation - Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
-
Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, Jeehoon Kang
In PLDI 2025: ACM SIGPLAN International Conference on Programming Language Design and Implementation
Recipient of PLDI 2025 Distinguished Paper Award - Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
-
Sunho Park, Jaehwang Jung, Janggun Lee, Jeehoon Kang
In PLDI 2025: ACM SIGPLAN International Conference on Programming Language Design and Implementation - Destabilizing Iris
- Tree Borrows
- RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers
- Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
- Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
- Modal Abstractions for Virtualizing Memory Addresses
-
Ismail Kuru, Colin S. Gordon
In OOPSLA 2025: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications - Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection
-
Alexandre Moine, Arthur Charguéraud, François Pottier
In TOPLAS 2025: ACM Transactions on Programming Languages and Systems - Context-Dependent Effects in Guarded Interaction Trees
-
Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal
In ESOP 2025: European Symposium on Programming - The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
- Tail Modulo Cons, OCaml, and Relational Separation Logic
-
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer
In POPL 2025: ACM SIGPLAN Symposium on Principles of Programming Languages - Program Logics à la Carte
- Approximate Relational Reasoning for Higher-Order Probabilistic Programs
- Data Race Freedom à la Mode
- Affect: An Affine Type and Effect System
- A Logical Approach to Type Soundness
-
Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal
In JACM 2024: Journal of the ACM, Volume 71, Issue 6, Article No. 40, November 2024 - Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly
- Verified Lock-Free Session Channels with Linking
- Multris: Functional Verification of Multiparty Message Passing in Separation Logic
- 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 - Refinement Composition Logic
-
Youngju Song, Dongjae Lee
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming - 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 - 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 - 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 - 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 - Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
- RefinedRust: A Type System for High-Assurance Verification of Rust Programs
- 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 - Unification for Subformula Linking under Quantifiers
-
Ike Mulder, Robbert Krebbers
In CPP 2024: ACM SIGPLAN International Conference on Certified Programs and Proofs - 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 - An Iris Instance for Verifying CompCert C Programs
-
William Mansky, Ke Du
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages - 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 - DisLog: A Separation Logic for Disentanglement
-
Alexandre Moine, Sam Westrick, Stephanie Balzer
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages - 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 - The Essence of Generalized Algebraic Data Types
- 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 - 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 - 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 - 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 - 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
In JACM 2023: Journal of the ACM, Volume 71, Issue 1, Article No. 3, February 2024 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - A Type System for Effect Handlers and Dynamic Labels
-
Paulo Emílio de Vilhena, François Pottier
In ESOP 2023: European Symposium on Programming - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom
- 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 - 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 - 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 - 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 - 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 - A Self-Dual Distillation of Session Types
-
Jules Jacobs
In ECOOP 2022: European Conference on Object-Oriented Programming - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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
- 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
- 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 - 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 - 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
In JFP 2023: Journal of Functional Programming, 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 - MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
- Mtac2: Typed Tactics for Backward Reasoning in Coq
- 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
- 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
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement
- 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 - 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
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation - 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 2025 Most Influential POPL Paper Award
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation
- Shaking Up the Foundations of Modern Separation Logic
-
Simon Spies
MPI-SWS and Saarland University, May 2025 - Proof Automation for Fine-Grained Concurrent Separation Logic
-
Ike Mulder
Radboud University Nijmegen, February 2025 - Formal Verification of Heap Space Bounds under Garbage Collection
-
Alexandre Moine
Inria and Université Paris Cité, September 2024 - Scaling Up Relaxed Memory Verification with Separation Logics
-
Hoang-Hai Dang
MPI-SWS and Saarland University, September 2024 - Verification of Concurrent Search Structures
-
Nisarg Patel
New York University, September 2024 - Guarantees by Construction
-
Jules Jacobs
Radboud University Nijmegen, June 2024 - 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 Otto Hahn Medal (Max Planck Society)
Recipient of 2024 Dr. Eduard Martin Prize (Saarland University) - Separation Logic for Concurrency and Persistency
-
Simon Friis Vindum
Aarhus University, December 2023 - Syntax and semantics of modal type theory
-
Daniel Gratzer
Aarhus University, October 2023 - Conflict-free Replicated Data Types have Abstract Data Types
-
Abel Nieto
Aarhus University, June 2023 - Designing and Proving Robust Safety of Efficient Capability Machine Programs
-
Aina Linn Georges
Aarhus University, June 2023 - Higher-Order Separation Logic for Distributed Systems and Security
-
Simon Oddershede Gregersen
Aarhus University, March 2023 - Proof of Programs with Effect Handlers
-
Paulo Emílio de Vilhena
Université Paris Cité, December 2022 - 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 - 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 - Sessions and Separation
-
Jonas Kastberg Hinrichsen
IT University of Copenhagen, March 2021 - Concurrent Separation Logics for Safety, Refinement, and Security
- 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 2020 Otto Hahn Medal (Max Planck Society)
Recipient of 2021 Dr. Eduard Martin Prize (Saarland University) - 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
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 - Logical Foundations Of Language Interoperability Between OCaml and C
-
Johannes Hostert
Master's thesis at Saarland University supervised by Derek Dreyer, July 2023 - Verifying a Barrier using Iris
-
Simcha van Collem
Bachelor's thesis at Radboud University Nijmegen supervised by Robbert Krebbers, March 2023 - 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
Logic and Semantics Group
Contact: Lars Birkedal
Contact: Lars Birkedal
Foundations of Programming Group
Contact: Derek Dreyer
Contact: Derek Dreyer
Department of Software Science
Contact: Robbert Krebbers
Contact: Robbert Krebbers
Grants
The Iris project has been supported by the following grants:
ModuRes
Modular Reasoning about Concurrent Higher-Order Imperative Programs
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
2015 ERC Consolidator Grant (more information)
CPV
Center for Basic Research in Program Verification
Villum Investigator grant (no. 25804) from The Villum Foundation from 2019-2025. (more information)