Iris Project

Lecture Notes

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 provides notes from a lecture introducing 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.

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