Test-of-Time Award für Ralf Jung

Über das Paper

Das Paper stellt Iris vor, ein vereinheitlichendes Framework für nebenläufige Trennungslogik höherer Ordnung, das im Rocq Prover (ehemals Coq) mechanisiert ist. Zu der Zeit, als Iris entstand, war das Feld der Trennungslogik gespalten, mit vielen unterschiedlichen und potenziell inkompatiblen Logiken, die mit massgeschneiderten Modellen entwickelt wurden. Diese erste Arbeit über Iris zeigte, wie einige Schlüsselkomponenten aus früheren Arbeiten – insbesondere partielle kommutative Monoide zur Darstellung von benutzerdefinierten Geisterzuständen (inspiriert durch das Views-Framework) und impredikative Invarianten höherer Ordnung (inspiriert durch schrittweise indizierte Modelle) – auf fruchtbare Weise kombiniert werden können, um eine Vielzahl anspruchsvoller Beweistechniken (wie z. B. „logisch atomare Tripel“) abzuleiten, die in früheren Logiken als primitiv eingebaut waren. Es war nur der erste Schritt in einer langen Reihe von Arbeiten einer reichen und vielfältigen Gemeinschaft von Iris-Entwickler*innen aus aller Welt. Dank der anschliessenden Arbeiten am Iris Proof Mode in Rocq ist Iris zu einem weit verbreiteten Werkzeug sowohl in der Programmuntersuchung als auch in der Metatheorie von Programmiersprachen geworden, mit Anwendungen, die von funktionalen Korrektheitsnachweisen für Low-Level-Systemcode (z. B. Hypervisoren, absturzsichere Systeme, schwache Speicher-Datenstrukturen) bis hin zu erweiterbaren semantischen Soundness-Nachweisen für High-Level-Systeme (z. B. Rust, OCaml, Scala) reichen.