Iris Project

Tutorial 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.

Below we list some tutorial material, which can be used as an introduction to Iris. The lecture notes have been used in an M.Sc. level course at Aarhus University. See the iris-project.org page for an overview of research that uses Iris one way or another.

POPL'18 Tutorial

    Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic
    Jacques-Henri Jourdan, Robbert Krebbers

Lecture Notes

    Lecture Notes on Iris: Higher-Order Concurrent Separation Logic
    Lars Birkedal, Aleš Bizjak

Course Plan with Slides

Week Day Lecture Literature Slides Hand-in Exercises
1 Day 1 Intro + Operational Semantics ILN Sec. 1+2  lecture1  
Day 2 Basic Logic of Resources ILN Sec. 3  lecture2 ILN Ex. 3.2
2 Day 1 Basic Separation Logic: Hoare Triples ILN Sec. 4.0  lecture3  
Day 2 Basic Separation Logic: Proving Pointer Programs ILN Sec. 4.1  lecture4 ILN Ex. 4.1, 4.2, 4.5, 4.11, 4.21
3 Day 1 Basic Separation Logic: Abstract Data Types ILN Sec. 4.2  lecture5  
Day 2 Case Study: foldr ILN Sec. 4.3  lecture6  ILN Ex. 4.29, 4.34
4 Day 1 Later Modality ILN Sec. 5  lecture7   
Day 2 Always Modality ILN Sec. 6  lecture8 ILN Ex. 5.3, 6.2 item (1) (2) and (4)
5 Day 1 Concurrency: par + invariants  ILN Sec. 7.1 + 7.2  lecture9  
Day 2 Concurrency: ghost state ILN Sec. 7.4 + 7.5  lecture10 ILN Ex. 7.6, 7.24 item (3), 7.29, 7.32 (the first triple)
6 Day 1 Concurrency: Case Study: spin lock + concurrent bag ILN Sec. 7.6  lecture11  
Day 2 Concurrency: Case Study: counter modules ILN Sec. 7.7  lecture12 ILN Ex. 7.37, 7.42.
7 Day 1 Weakest preconditions and fancy update modality  ILN Sec. 8.1 + 8.2  lecture13  
Day 2 Concurrency: Case Study: concurrent stack with helping ILN Sec. 10  lecture14 ILN Ex. 7.43 (the one for incr), 7.47, 7.49 (the two specs for read).