Nominal Coalgebraic Data Types with Applications to Lambda CalculusArticle
Authors: Alexander Kurz ; Daniela Luan Petrişan ; Paula Severi ; Fer-Jan de Vries
0000-0002-8685-5207##NULL##NULL##NULL
Alexander Kurz;Daniela Luan Petrişan;Paula Severi;Fer-Jan de Vries
We investigate final coalgebras in nominal sets. This allows us to define
types of infinite data with binding for which all constructions automatically
respect alpha equivalence. We give applications to the infinitary lambda
calculus.
Henning Urbat;Daniel Hausmann;Stefan Milius;Lutz Schröder, International Conference on Concurrency Theory, Nominal Büchi Automata with Name Allocation, pp. 16-, 2021, 10.4230/lipics.concur.2021.4.
Jasmin Christian Blanchette;Lorenzo Gheri;Andrei Popescu;Dmitriy Traytel, 2019, Bindings as bounded natural functors, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-34, 10.1145/3290335, https://doi.org/10.1145/3290335.