2025/11/04 by Cerda, Rémy
#D.3.3 #F.3.3 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2511.02595
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 Lambdaabc of abc-infinitary lambda-terms (for a, b, c in 0,1) and of capture-avoiding substitution on alpha-equivalence classes of such terms.