The Iris Tutorial in Lean
This tutorial introduces the Iris separation logic framework in Lean, using the iris-lean development. It is adapted from the Iris tutorial originally developed at Aarhus University.
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.
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