2025 Alonzo Church Award: Unifying Lambda Calculus Research

Paul Blain Levy received the 2025 Alonzo Church Award for his groundbreaking work on the Call-by-Push-Value (CBPV) calculus. His research unified the separate streams of pure logical and applied effectful lambda calculus research. CBPV serves as a unifying framework for studying computational and logical phenomena, including effects, polarization, term normalization, type isomorphisms, and program transformations. Levy's contributions span algebraic datatypes, operational semantics, denotational semantics, and equational theories, significantly advancing the semantic theory of lambda calculus and its application to programming language modeling.