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
4.
HeapLang
4.1.
Introduction
4.2.
The HeapLang Interpreter (Optional)
4.3.
Pure Constructs
4.4.
References
4.5.
Concurrency
←
3. Pure Propositions
4.1. Introduction
→
4. HeapLang
🔗
4.1.
Introduction
4.2.
The HeapLang Interpreter (Optional)
4.3.
Pure Constructs
4.4.
References
4.5.
Concurrency
←
3. Pure Propositions
4.1. Introduction
→