Finitary Corecursion for the Infinitary Lambda Calculus

Stefan Milius, Thorsten Wißmann

Kurz et al. have recently shown that infinite $\lambda$-trees with finitely many free variables modulo $\alpha$-equivalence form a final coalgebra for a functor on the category of nominal set…