Profinite λ-terms and higher-order regular languages

Prelegent(ci)

Vincent Moreau

Afiliacja

Tallinn University of Technology

Język referatu

angielski

Termin

6 listopada 2026 12:15

Pokój

p. 5450

Tytuł w języku polskim

λ-terms proskończone i regularne języki wyższego rzędu

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

For several years now, there has been a growing connection between automata theory and λ-calculus, in terms of syntax, semantics and logic. We introduce profinite λ-terms, a higher-order generalization of the notion of profinite word found at the heart of automata theory. These assemble into a cartesian closed category which verifies an adequate universal property with respect to finite models, justifying the denomination of profinite λ-calculus. We show how profinite λ-terms are related to higher-order languages, as introduced by Salvati, via Stone duality. Moreover, we show that higher-order regular language are robust, by providing a natural criterion for cartesian closed categories to recognize exactly these languages.

---