Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 20-minute conference talk from POPL 2025 that introduces the concept of interaction equivalence in the untyped λ-calculus. Presented by researchers Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, and Gabriele Vanoni from various French institutions, this presentation addresses limitations of contextual equivalence when considering computational costs. Learn how the authors develop a novel approach inspired by game semantics that observes interaction steps between terms and contexts while ignoring internal steps. Discover how they prove interaction equivalence forms an equational theory characterized by Böhm tree equality (ℬ), marking the first observational characterization of ℬ without requiring additional context features like non-determinism. The talk covers innovative refinements of the Böhm-out technique and intersection types to establish these results. Part of the ACM SIGPLAN POPL 2025 conference held January 19-25, 2025.
