13 juin 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).