June 13, 2022

Nguyễn Lê Thành Dũng (LIX)

In this talk, I will argue that some natural questions on the expressive power of typed λ-calculi (minimalistic functional programming languages) actually pertain not to programming languages, but to automata theory (or “finite-state computation”). After briefly mentioning the results in my PhD thesis on type systems based on linear logic, I will explain how recursion schemes and transducer theory motivate a conjecture on the functions definable in the simply typed λ-calculus (in a certain way that goes back at least to Statman’s work in the 1980s, but about which very little is known).
This is joint work with Pierre Pradic (Swansea University).