In their sixth episode, hosts of the "Type Theory Podcast" "speak with Professor Aaron Stump from the University of Iowa. [They] 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."

Additional material available on the podcast site.

Stay tuned for an upcoming UI-produced podcast entitled "Masters of Type Theory."