Test-of-Time Award for Ralf Jung

About the paper

The paper introduces Iris, a unifying framework for higher-order concurrent separation logic mechanised in the Rocq Prover (formerly Coq). At the time Iris came along, the field of separation logic had become fractured, with many different and potentially incompatible logics being developed with bespoke models. This first paper on Iris showed how a few key ingredients from prior work – most notably, partial commutative monoids for representing user-defined ghost state (inspired by the Views framework) and higher-order impredicative invariants (inspired by step-indexed models) – could be fruitfully combined to derive a wide variety of sophisticated proof techniques (such as "logically atomic triples") that were built in as primitive in prior logics. It was just the first step in a long line of work by a rich and diverse community of Iris developers from around the world. Thanks to subsequent work on the Iris Proof Mode in Rocq, Iris has become a widely-used tool in both program verification and programming language meta-theory, with applications ranging from functional correctness proofs for low-level systems code (e.g. hypervisors, crash-safe systems, weak-memory data structures) to extensible semantic soundness proofs for high-level systems (e.g. Rust, OCaml, Scala).