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

9. Arrays in HeapLang

←8. The Later Modality and Recursive Functions 10. Resource Algebras→

9. Arrays in HeapLang🔗

This chapter has not yet been ported. The Rocq source is iris-tutorial/theories/arrays.v.

←8. The Later Modality and Recursive Functions 10. Resource Algebras→