On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus

This conference talk explores the decidability of the reachability problem for finitary PCF and its extensions in functional programming. Discover how Naoki Kobayashi from the University of Tokyo provides simple proofs of undecidability for four extensions of finitary PCF with side effects (exceptions, algebraic effects, and references). Learn about a novel decidable fragment for the extension with references using a type system - the first non-trivial decidable fragment featuring higher-order recursive functions containing reference cells. The presentation examines the theoretical foundations that impact automated verification tools for functional programs and analyzes the sources of undecidability in these systems. Presented at the POPL 2025 conference (January 19-25, 2025), this 19-minute talk provides valuable insights for researchers and developers working with simply-typed lambda calculus and program verification.