Alonzo Church Award

The Alonzo Church Award for Outstanding Contributions to Logic and Computation was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS) (until 2022). The award is for an outstanding contribution represented by a paper or small group of papers within the past 25 years.

Please see the latest Call for Nominations.

The 2025 Alonzo Church Award for Outstanding Contributions to Logic and Computation

The European Association for Computer Science Logic (EACSL), the European Association for Theoretical Computer Science (EATCS), and the ACM Special Interest Group for Logic and Computation (SIGLOG) are pleased to announce that the 2025 Alonzo Church Award for Outstanding Contributions to Logic and Computation is presented to

Paul Blain Levy 

for his fundamental study of effectful λ-calculi through the Call-by-Push-Value calculus.

The awardee book and paper are:
  • Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation 2, Springer 2004, ISBN 1-4020-1730-8
  • Paul Blain Levy. Call-by-Push-Value: Decomposing call-by-value and call-by-name. High.-Order Symb. Comput. 19(4): 377-414 (2006)
Initiated by Alonzo Church, the research programme into the λ-calculus as an abstract model of computation has spurred volumes of fundamental research in logic and computation. By the end of the 20th century, the studies of the λ-calculus in its purely logical form and its applied effectful form bifurcated. In an outstanding contribution, Levy has reunited the many existing research streams into the study of one subsuming calculus: Call-by-Push-Value (CBPV). Levy developed and presented an extraordinarily large body of evidence spanning a cross-section of the semantic theory of the λ-calculus and its application to programming language modelling, including: algebraic datatypes, operational semantics, denotational semantics, and equational theories. To date, CBPV remains a unifying starting point in the study of computational and logical phenomena, including: effects, polarisation, term normalisation, type-isomorphisms, and program transformations. In addition to its scientific contribution, the nominated monograph is a unique access-point into the culmination of decades of logic and programming language semantics.