activity
20182022
most citedMonotone recursive types and recursive data representations in Cedille

2 citations · 3 across the 7 of their papers we have counts for

collaborators
Showing 2019Show all

1 paper · 1 filter

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