+ This paper introduced Iris, a unifying framework for higher-order concurrent separation logic mechanized 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 type systems (e.g. Rust, OCaml, Scala).
0 commit comments