17 citations · 36 across the 16 of their papers we have counts for
Showing 2019Show all
2 papers · 1 filter
cs.LO2019
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
Aaron Stump
Cedille is a relatively recent tool based on a Curry-style pure type theory, without a primitive datatype system. Using novel techniques based on dependent intersection types, indu…
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 (…