The Duality of λ-Abstraction

Explore a 19-minute video presentation from POPL 2025 where researchers Vikraman Choudhury and Simon J. Gay introduce their work on the duality of lambda abstraction. Discover how higher-order continuations give rise to coexponentials, similar to how higher-order functions produce exponentials. Learn about their extension of call-by-value simply-typed lambda-calculus with covalues, coabstraction, and coapplication. The presentation covers the semantics developed using axiomatic structure of continuations, computational interpretation through speculative execution and backtracking, derivation of classical control operators, and applications of this duality in programming. Access supplementary materials including the full paper, artifact repository, and additional resources to deepen your understanding of type theory, category theory, continuations, control effects, and classical logic through the Curry-Howard correspondence.