We show that various classes of languages and functions from automata theory can be equivalently defined using λ-calculi with substructural types. For instance, we characterize regular string-to-string functions with affine types, and star-free languages with non-commutative types. These results have few direct precedents, but they are analogous to the field of implicit computational complexity, except with automata instead of complexity classes. Our starting point is the little-known fact that the predicates definable over Church-encoded strings in the simply typed λ-calculus are exactly the regular languages (Hillebrand & Kanellakis, LICS’96). More recently, similar ideas have played a prominent role in higher-order model checking.
This is joint work with Pierre Pradic (University of Oxford).
The seminar will take place online. More information is available at: https://team.inria.fr/partout/seminar/