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