The Iris Tutorial in Lean
This is a Lean port of the Iris tutorial originally developed at Aarhus University as a Rocq tutorial for the Iris separation logic framework.
The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming language theory and discrete mathematics will be beneficial. Additionally, basic knowledge of the Lean prover is assumed; this port replaces the Rocq proofs of the original with Lean 4 proofs against the iris-lean port of Iris.
Contents
- 1. Recommended Learning Path
- 2. Basics of Iris
- 3. Pure Propositions
- 4. HeapLang
- 5. Specifications
- 6. The Persistently Modality
- 7. Linked Lists
- 8. The Later Modality and Recursive Functions
- 9. Arrays in HeapLang
- 10. Resource Algebras
- 11. Invariants
- 12. Timeless Propositions
- 13. Structured Concurrency
- 14. Counter and the Authoritative Camera
- 15. Spin Lock
- 16. Ticket Lock
- 17. Adequacy
- 18. Additional Material
- 19. Guarded Recursive Predicates
- 20. Merge Sort
- 21. Defining Resource Algebras from Scratch
- 22. Ordered Families of Equivalences (OFEs)
- 23. Ticket Lock — Advanced Tactics
- Index