Implicit automata in typed λ-calculi

What predicates or functions can be defined by terms of a certain type (think "string -> bool") in a given language? For terminating calculi arising from the proofs-as-programs correspondence, the answer is not "all computable functions". The field of Implicit Computational Complexity ( https://tel.archives-ouvertes.fr/tel-02978986 ) has demonstrated that interesting complexity classes can be characterized this way using type systems deliberately designed for this purpose, often based on some variant of linear logic.

In the work presented here, we focus on typed λ-calculi (some of which are linear or affine) that were *not* introduced with ICC in mind. From Hillebrand and Kanellakis's theorem (1996) on regular languages in the simply typed λ-calculus using Church encodings, and similar ideas in higher-order model checking, we draw the lesson that connections with various finite-state devices ("automata") arise more naturally in this context than with computational complexity. This talk will focus in particular on the relationships that we discovered between non-commutative/ordered types and aperiodicity (star-free languages and first-order string transductions). I also hope to offer a glimpse of the algebraic and compositional character of modern automata theory, far from a mere collection of combinatorial recipes to study ad-hoc machine models.

All this is joint work with Cécilia Pradic (Swansea University).