In this talk I will give an overview of the Iris project. Firstly, I will present the Iris base logic, which is a small resourceful logic that can be used to develop complex separation logics in a layered way. This base logic only comprises the assertion layer of vanilla separation logic, plus a handful of simple modalities. The much fancier logical mechanisms of the Iris program logic, such as Hoare triples and impredicative invariants, can be understood as merely derived forms in this base logic.

Secondly, I will show that our base logic is effective for formalization in Coq. I will show how to extend the Coq proof assistant with (spatial and non-spatial) named proof contexts and high-level tactics for reasoning in the Iris base logic. This way, we can seamlessly formalize the meta theory of the various layers of Iris, and use Iris for non-trivial applications such formalization of the Rust type system, (binary) logical relations, and concurrent data structures.