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.PL2019
Elaborating Inductive Definitions and Course-of-Values Induction in Cedille
Christopher Jenkins, Colin McDonald, Aaron Stump
In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style type theory, it is possible to generically λ-encode inductive datatypes which support course-of-values (…
cs.PL2018
Spine-local Type Inference
Christopher Jenkins, Aaron Stump
We present spine-local type inference, a partial type inference system for inferring omitted type annotations for System F terms based on local type inference. Local type inference…