{"ID":2846241,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.02595","arxiv_id":"2511.02595","title":"Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi","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.","short_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-c...","url_abs":"https://arxiv.org/abs/2511.02595","url_pdf":"https://arxiv.org/pdf/2511.02595v1","authors":"[\"Rémy Cerda\"]","published":"2025-11-04T14:18:32Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.PL\"]","methods":"[]","has_code":false}