- Remaining examples from ILN
- Ch. 16 - fixpoints
- Detailed description of cmra with excercises on defining new ones.
- Defining a discrete cmra
- What is an ofe
- Generic cmra
- Higher order cmra
- Internal equivalence and validity (Plainly, SIProp)
- Inner workings of BI and using Iris proofmode on other logics.
- Incompatability of excluded middle.
- How to define a new language in Iris.
- Defining new modalities
- Run through the relevant typeclasses