Implicit automata in λ-calculi

Prelegent(ci)

Pierre Pradic

Afiliacja

ENS Lyon

Termin

24 czerwca 2020 14:15

Pokój

p. 5050

Tytuł w języku angielskim

joint work with Lê Thành Dũng

Seminarium

Seminarium „Teoria automatów”

---

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.

---