research
∙
12/15/2021
Simulating Large Eliminations in Cedille
Large eliminations provide an expressive mechanism for arity- and type-g...
share
research
∙
01/24/2021
Relational Type Theory (All Proofs)
This paper introduces Relational Type Theory (RelTT), a new approach to ...
research
∙
05/01/2020
Efficient lambda encodings for Mendler-style coinductive types in Cedille
In the calculus of dependent lambda eliminations (CDLE), it is possible ...
research
∙
01/09/2020
Monotone recursive types and recursive data representations in Cedille
Guided by Tarksi's fixpoint theorem in order theory, we show how to deri...
research
∙
10/24/2019
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
Cedille is a relatively recent tool based on a Curry-style pure type the...
research
∙
03/19/2019
Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to Cedille
In CDLE, a pure Curry-style type theory, it is possible to generically d...
research
∙
11/29/2018
Course-of-Value Induction in Cedille
In the categorical setting, histomorphisms model a course-of-value recur...
research
∙
11/04/2018
Syntax and Typing for Cedille Core
This document specifies a core version of the type theory implemented in...
research
∙
06/12/2018
Syntax and Semantics of Cedille
This document presents the syntax, classification rules, realizability s...
research
∙
05/25/2018
Spine-local Type Inference
We present spine-local type inference, a partial type inference system f...
research
∙
03/21/2018
Generic Zero-Cost Reuse for Dependent Types
Dependently typed languages are well known for having a problem with cod...
research
∙
03/06/2018
Efficient Mendler-Style Lambda-Encodings in Cedille
It is common to model inductive datatypes as least fixed points of funct...
research
∙
02/02/2018