Max Planck Researchers honored for outstanding contributions to logic and computation
MPI-SWS faculty member Derek Dreyer and nine of his collaborators (including notably UdS/MPI alumnus Ralf Jung, as well as former MPI-SWS postdocs Jacques-Henri Jourdan and Aaron Turon and UdS/MPI student David Swasey) have received the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation for their seminal work on the Iris framework for higher-order concurrent separation logic.
Specifically, the following four papers were recognized:
- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer: “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning”. POPL 2015.
- Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer: “Higher-order ghost state”. ICFP 2016.
- Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal: “The Essence of Higher-Order Concurrent Separation Logic”. ESOP 2017.
- Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer: “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. J. Funct. Program. 28 (2018).
The Church Award has been given out since 2016, and has typically been given to papers that were 20-25 years old (to allow time for foundational work on logic to have major impact). In this case, however, the four awarded Iris papers were published only 5-8 years ago! In that relatively short period of time, Iris has served as a springboard for a huge amount of research in semantics and program verification, including over 70 papers in top venues (see the Iris project page), and it has been adopted as a core verification technology by a multitude of research groups around the world, as well as the systems verification company BedRock Systems. More details about the Alonzo Church Award and about the 2023 Church Award.
Originally published at Max Planck Institute for Software Systems