17 citations · 36 across the 16 of their papers we have counts for
19 papers
Simulating Large Eliminations in Cedille
Christopher Jenkins, Andrew Marmaduke, Aaron Stump
Large eliminations provide an expressive mechanism for arity- and type-generic programming. However, as large eliminations are closely tied to a type theory's primitive notion of i…
Relational Type Theory (All Proofs)
Aaron Stump, Benjamin Delaware, Christopher Jenkins
This paper introduces Relational Type Theory (RelTT), a new approach to type theory with extensionality principles, based on a relational semantics for types. The type constructs o…
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…
Monotone recursive types and recursive data representations in Cedille
Christopher Jenkins, Aaron Stump
Guided by Tarksi's fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time roll and unroll operations within Cedille, an impredicative,…
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…
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 (…