The Iris Tutorial in Lean

The Iris Tutorial in Lean

Table of 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

1. Recommended Learning Path

← The Iris Tutorial in Lean 2. Basics of Iris→

1. Recommended Learning Path🔗

To get a good understanding of the fundamental concepts of Iris, it is recommended to study the following chapters in the given order.

← The Iris Tutorial in Lean 2. Basics of Iris→