17 citations · 36 across the 16 of their papers we have counts for
Showing 2021Show all
2 papers · 1 filter
cs.PL2021
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…
cs.LO2021
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…