Showing cs.PLShow all
3 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.PL2018
Generic Zero-Cost Reuse for Dependent Types
Larry Diehl, Denis Firsov, Aaron Stump
Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed var…
cs.PL2018
Zero-Cost Coercions for Program and Proof Reuse
Larry Diehl, Aaron Stump
We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type t…