17 citations · 36 across the 16 of their papers we have counts for
Showing 2020Show all
2 papers · 1 filter
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★ 2 cited
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,…