4 papers
Course-of-Value Induction in Cedille
Denis Firsov, Larry Diehl, Christopher Jenkins +1
In the categorical setting, histomorphisms model a course-of-value recursion scheme that allows functions to be defined using arbitrary previously computed values. In this paper, w…
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…
Variations on Noetherianness
Denis Firsov, Tarmo Uustalu, Niccolò Veltri
In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda…