Derek Dreyer erhält den ICFP Most Influential Paper Award

Bild der Preisverleihung (© MPI-SWS)

Derek Dreyer, wissenschaftlicher Mitarbeiter am MPI-SWS, wurde für seine 2016 gemeinsam mit dem MPI-SWS-Alumnus Ralf Jung sowie Robert Krebbers und Lars Birkedal verfasste Arbeit „Higher-Order Ghost State“ mit dem „Most Influential ICFP Paper Award“ ausgezeichnet. Die Auszeichnung würdigt den nachhaltigen Einfluss der Arbeit auf das Programmlogik-Framework Iris, das zu einer wichtigen Grundlage für die Forschung im Bereich der Softwareverifikation geworden ist. Diese Auszeichnung ergänzt den „Most Influential POPL Paper Award“ für die Iris-1.0-Arbeit (POPL’15) sowie den „Alonzo Church Award“, den sie 2023 für die vier zentralen Paper zu den Grundlagen von Iris erhielten.

Der „ACM SIGPLAN Most Influential ICFP Paper Award“ ist eine retrospektive Auszeichnung – er wird jedes Jahr an den Beitrag verliehen, der als der einflussreichste der ICFP-Konferenz zehn Jahre zuvor angesehen wird.

Ein Video von der Preisverleihung findet sich hier: https://www.youtube.com/live/wn88R35yqeY?t=26630s

Begründung für die Auszeichnung: „Higher-Order Ghost State“ stellt einen wichtigen Meilenstein für das weit verbreitete Programmlogik-Framework Iris dar. Umgangssprachlich als „Iris 2.0“ bekannt, liefert die Arbeit ein wesentliches Merkmal: die Möglichkeit, beliebige Prädikate der Separationslogik höherer Ordnung in Ghost-Variablen zu speichern. Dieses Merkmal wird mithilfe von guarded Recursion und einer neuen algebraischen Struktur namens „Cameras“ begründet – vereinfacht gesagt handelt es sich dabei um eine Verallgemeinerung von PCMs mit einer Form von Step Indexing. Der „Higher-Order Ghost State“ erwies sich später als wesentlicher Baustein, aus dem sich weitere Funktionen wie impredikative Invarianten und schwächste Preconditions ableiten ließen. Seine weitreichende und nachhaltige Bedeutung zeigt sich in den (derzeit) 165 Papern, die Iris in irgendeiner Form nutzen, darunter 45 POPL-, 29 PLDI-, 25 ICFP- und 20 OOPSLA-Paper.