MPI-SWS faculty member Derek Dreyer and his collaborators (including MPI-SWS alumni Ralf Jung, David Swasey, and Aaron Turon) have received the 2025 Most Influential POPL Paper Award for their POPL 2015 paper, "Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning" (https://iris-project.org/pdfs/2015-popl-iris1-final.pdf).  This comes on top of the Alonzo Church Award that they received in 2023 for the four core papers on the foundations of Iris.

The ACM SIGPLAN Most Influential POPL Paper Award is a retrospective award—it is given each year to the paper deemed most influential from the POPL conference 10 years earlier.

Award citation: 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).

A video of the award presentation can be found here: https://www.youtube.com/live/ZKwpY0g9Lo8?si=scSr-qC9C44huJ_f&t=28949

MPI-SWS scientific director Derek Dreyer was appointed as a Fellow by the Association for Computing Machinery (ACM), the largest computer science association in the world. Derek, who leads the “Foundations of Programming” research group, received this honor for his contributions to the logical and semantic foundations of programming languages.

The ACM Fellows program recognizes the 1% of ACM members who have made the most outstanding achievements in the field of computer and information technology. Worldwide 55 new ACM Fellows were elected this year, thirteen of them in Europe and four in Germany.

Further Information: 

• https://www.acm.org/media-center/2025/january/fellows-2024


• https://awards.acm.org/fellows/award-winners


• https://www.mpi-sws.org/people/dreyer/

Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 9 papers accepted to POPL 2025.  This is the eighth year in a row that MPI-SWS researchers have published 5+ papers in POPL. Furthermore, as of this year, MPI-SWS faculty member Derek Dreyer has published 25 papers at POPL----a new record!  Congratulations to all our POPL authors!

Congratulations to all our POPL authors!

• Data Race Freedom à la Mode by Aina Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer   ***Recipient of a distinguished paper award.


• A quantitative probabilistic relational Hoare logic by Martin Avanzini, Gilles Barthe, Benjamin Gregoire, Davide Davoli


• Automating equational proofs in Dirac notation by Yingte Xu, Gilles Barthe, Li Zhou


• Preservation of speculative constant-time by compilation by Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, Vincent Laporte


• Sound and Complete Proof Rules for Probabilistic Termination by Rupak Majumdar, V.R. Sathiyanarayana


• RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency by Pavel Golovin, Michalis Kokologiannakis, Viktor Vafeiadis


• Model Checking C/C++ with Mixed-Size Accesses by Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis


• Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning by Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan


• Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
  Yonghyun Kim, Minki Cho, Jaehyung Lee, Jinwoo Kim, Taeyoung Yoon, Youngju Song, Chung-Kil Hur