In our sixth episode, we speak with Professor Aaron Stump from the University of Iowa. We discuss Cedille, a proof assistant based on the Calculus of Dependent Lambda Eliminations, which allows impredicative lambda-encodings to be used for dependently typed programming, instead of a separate notion of inductive datatypes.

Reading:

- From Realizability to Induction via Dependent Intersection by Aaron Stump. Under review.
- Project Report: Dependently typed programming with lambda encodings in Cedille by Ananda Guneratne, Chad Reynolds, and Aaron Stump. In post-proceedings for TFP 2016.
- The Calculus of Dependent Lambda Eliminations by Aaron Stump. Under review for the Journal of Functional Programming.
- Efficiency of Lambda-Encodings in Total Type Theory by Aaron Stump and Peng Fu. In the Journal of Functional Programming, 2016.
- The Calculus of Implicit Constructions by Alexandre Miquel. In TLCA 2001.
- Reasoning about functional programs and complexity classes associated with type disciplines by Daniel Leivant. In Foundations of Computer Science, 1983

Additional links:

- Verified Functional Programming in Agda by Aaron Stump
- Aaron Stump’s Web page