Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for fault-tolerant systems code, and a safety proof for a realistic subset of the Rust programming language.

In this tutorial, you will learn how use the Iris framework to reason about concurrent programs. This tutorial will be hands-on: we will use the Coq implementation of Iris to mechanize our proofs. It is recommended to come with Coq and Iris pre-installed on your machine so that you can play with Iris yourself. You can follow the installation instructions in the tutorial exercises git repository.