Showing 2020 · cs.PLShow all
2 papers · 2 filters
cs.PL2020
Efficient lambda encodings for Mendler-style coinductive types in Cedille
Christopher Jenkins, Aaron Stump, Larry Diehl
In the calculus of dependent lambda eliminations (CDLE), it is possible to define inductive datatypes via lambda encodings that feature constant-time destructors and a course-of-va…
cs.PL2020
Monotone recursive types and recursive data representations in Cedille
Christopher Jenkins, Aaron Stump
Guided by Tarksi's fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time roll and unroll operations within Cedille, an impredicative,…