Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic

Robbert Krebbers

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 object capabilities, and a safety proof for a realistic subset of the Rust programming language. In this talk I will give an introduction to Iris and its implementation in Coq.

---

Previous: Albert ten Napel | Dynamic instances for algebraic effects and handlers
Next: Wiebe van Geest | Dependent Types for Invariants in Session Types