4 citations · 5 across the 5 of their papers we have counts for
8 papers · 1 filter
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…
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 (…
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…
Efficient Mendler-Style Lambda-Encodings in Cedille
Denis Firsov, Richard Blair, Aaron Stump
It is common to model inductive datatypes as least fixed points of functors. We show that within the Cedille type theory we can relax functoriality constraints and generically deri…
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…
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…