Unification via the Segal condition internally to the λ-calculus
Vincent Moreau
Tallinn University of Technology
https://compose.ee/vincent/
Date(s) : 01/10/2026 iCal
11h00 - 12h30
In this talk, I present ongoing work relating unification, simplicial structures, and higher-order regular languages. My starting point is the fact that Higman’s order between finite words can naturally be enhanced to a structure of category that internalizes in the simply typed λ-calculus. In turn, it can be decomposed as a cocategory, which we reconstruct in a principled way via the bar construction. Finally, I will show that the associated Segal condition amounts to the existence of a number of colimits in the free cartesian closed category, akin to pushout-product constructions, and that these have a natural interpretation in terms of unification. If time permits, I will talk about directions to extend these internal categorical structures from words to trees with an eye towards approximants and Böhm trees.
Emplacement
Luminy - LIS, salle 04.02
Catégories



