Profinite λ-terms and higher-order regular languages

Speaker(s)

Vincent Moreau

Affiliation

Tallinn University of Technology

Language of the talk

English

Date

Nov. 6, 2026, 12:15 p.m.

Room

room 5450

Title in Polish

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

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---