1 paper
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 (…