Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi
R\'emy Cerda (Aix-Marseille Universit\'e, CNRS, I2M)

TL;DR
This paper extends nominal techniques to define mixed inductive-coinductive data types with variable binding, enabling a nominal description of infinitary lambda-terms and capture-avoiding substitution.
Contribution
It introduces mixed binding signatures and corresponding types, extending prior work to infinitary lambda-calculi with variable binding.
Findings
Nominal description of abc-infinitary lambda-terms.
Extension of corecursion principles to mixed inductive-coinductive types.
Formalization of capture-avoiding substitution on alpha-equivalence classes.
Abstract
Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that alpha-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce "mixed" binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets Lambda_abc of abc-infinitary lambda-terms (for a, b, c in {0,1}) and of capture-avoiding substitution on alpha-equivalence classes of such terms.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Homotopy and Cohomology in Algebraic Topology · Logic, Reasoning, and Knowledge
