Alonzo Church Award for Robbert Krebbers

Robbert Krebbers, associate professor of Software Science at Radboud University, will receive the Alonzo Church Award 2023. The prize is awarded annually by the Association for Computing Machinery (ACM SIGLOG) and the European organisations for logic in computer science (EATCS, EACSL and the Kurt Gödel society) to researchers who have made influential contributions to logic in computer science over the past 25 years.

Krebbers receives the award together with colleagues from the Max Planck Institute for Software Systems in Germany, Aarhus University in Denmark, ETH Zurich in Switzerland, CNRS Paris in France, and the University of Wrocław in Poland. The researchers received the prize for four publications on the development of the Iris logic, for determining the correctness of computer programs.

Separation logic

A critical challenge faced by computer science researchers is to build computer programs that never crash, never make mistakes, and are secure. In reality, however, this is difficult to achieve because current computer programs are complex and often run several tasks at the same time (in parallel).

Robbert Krebbers' research focuses on the use of mathematical methods to prove that a computer program works correctly. The challenge is to develop mathematical concepts that can handle the complexity of contemporary computer programs and programming languages like Rust, C and Go, such as running parallel tasks. To make this possible, Krebbers and colleagues break up the mathematical proof into separate parts that precisely match up with the parts of the computer program. They use the mathematical concept of separation logic, which is the basis of the Iris logic for which the researchers received the Alonzo Church Award.

Robbert Krebbers: “We can make an analogy between programming a computer program and building a Lego structure. Imagine working with several people on a Lego construction. In that case, it is important that you agree together on how to approach this, so that you do not work against each other. We make a plan with rules for each Lego brick and builder: who is responsible for laying which bricks? This plan prevents mistakes.

With our tool Iris we can make such a plan for the different parts of a computer program: we use mathematical precision to write the logical rules that are necessary to ensure that the computer program works without errors. The use of separation logic allows us to write down the logical rules for each part of the program, rather than the entire computer program. You can then use Iris to check whether each program component complies with the logical rules, and Iris ensures that the entire computer program works without errors.”


Iris is now widely used in research. It is also being taken up within the industry: researchers at Meta (from Facebook), JetBrains and BedRock Systems have used Iris to determine the correctness of some of their parallel algorithms. Together with the developers of Iris, and researchers in Cambridge, among others, Krebbers uses Iris to determine the correctness of security-critical parts of Google's Android.

Robbert Krebbers: “Iris started as purely theoretical research, but I am very proud of the practical applications it now has. I think that's why we’ll receive the Alonzo Church Award. A nice recognition for our work!”

The Alonzo Church Award will be presented on 12 July at ICALP 2023 in Paderborn, Germany.

Literature reference


  • 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”. ACM SIGPLAN Symposium on Principles of Programming Languages, 2015. 
  • Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer: “Higher-order ghost state”. ACM SIGPLAN International Conference on Functional Programming, 2016. 
  • Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal: “The Essence of Higher-Order Concurrent Separation Logic”. European Symposium on Programming, 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”. Journal of Functional Programming 28, 2018.