2025 Alonzo Church Award: Paul Blain Levy for Call-by-Push-Value (CBPV)

CBPV splits evaluation into value vs computation, offering a powerful foundation that:

  1. Unifies CBV/CBN under one semantics-preserving translation,

  2. Supports both syntax-level and semantics-level reasoning,

  3. Admits a clear categorical interpretation

  4. Enhances clarity in handling effects and evaluation order.

CBPV:

• Encodes effects explicitly via separation of values and computations.

• Effects live in the F A (computation) types.

• Uses a monad (or algebraic theory) to model sequencing, effects, etc.

• thunk and force structure define an adjunction: U \dashv F : \mathcal{C} \leftrightarrows \mathcal{V}

Algebraic Effects:

• Treat effects as operations with laws—e.g. get, put, print, choose, etc.

• Combine effects via free algebras, effect handlers, and their corresponding Lawvere theories.

• Expressed categorically as:

• Effect signatures = operations,

• Algebra = model of those operations.

CBPV naturally supports algebraic effects because:

• The computation category C can be built from the free model of an algebraic theory, i.e. it’s the Kleisli category of a monad arising from algebraic operations.

• CBPV doesn’t enforce how the monad arises—so you can plug in any algebraic theory of effects.

• CBPV generalizes and supports algebraic effects seamlessly

It looks like a lambda calculus with effectful computations that can model imperative programming. I hadn't heard of it before either.

https://en.wikipedia.org/wiki/Call-by-push-value