Thursday 25 June 2020, 14:00, online: Implicit automata in typed λ-calculi, Tito (Lê Thành Dũng) Nguyễn (PhD student, LIPN, Univ. Paris Nord).

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 work will presented at ICALP 2020

See an associated paper.

This is joint work with Pierre Pradic (University of Oxford).