Implicit automata in λ-calculi

This work is part of an exploration of the expressiveness of
the simply-typed λ-calculus (STLC) and related substructural
variants (linear, affine, planar) using Church encodings of
datatypes. More specifically, we are interested in the connection
with automata theory for string transductions and languages.
After introducing and motivating the problems using Hillebrand
and Kanellakis's result on STLC-definable and regular
languages, I will discuss refinements we obtained for linear
λ-calculi. The focus will be put on the characterization of the
star-free languages as the functions string -> bool definable
in a non-commutative λ-calculus (the companion paper may
be consulted here https://hal.archives-ouvertes.fr/hal-02476219v2/document)
If time allows, I will briefly touch upon some further work on a
characterization of regular transductions as string -> string functions
definable in the affine λ-calculus.