Lecture Series on Higher-Order Concurrent Separation Logic

Software bugs cost billions and can have severe consequences for the infrastructure we rely on. Formally proving program correctness is therefore of paramount importance. Hoare logic provides a framework for modular verification of programs. Separation logic extends Hoare logic with a powerful concept: separation—program modules working on disjoint resources can be reasoned about in isolation from one another. Iris, the state-of-the-art Higher-Order Concurrent Separation Logic framework, extends this further by introducing reasoning principles such as higher-order impredicative invariants and user-defined ghost resources. These features are crucial for scaling the reasoning to highly concurrent programs with shared mutable state, featuring higher-order functions written in modern programming languages such as OCaml, Rust, and Go. This course is based on the Iris lecture notes and will enable students to specify and verify concurrent data structures and algorithms in Iris.