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.

In our fifth episode, we speak with Bob Constable from Cornell University. In addition to having been doctoral advisor to many of the leading researchers in programming languages, Bob leads the PRL research group in constructive type theory, which has produced the Nuprl proof assistant. In this interview, we discuss Nuprl and its underlying type theory, along with the intellectual context within which they have developed.

In our fourth episode, we speak with Stephanie Weirich from the University of Pennsylvania on the Zombie language and Dependent Haskell. Stephanie is a long-time contributor to Haskell, having been involved in the design and implementation of features such as generalized algebraic datatypes, higher-rank polymorphism, type families, and promoted datatypes. She has also been a participant in Trellys, a project with the goal of combining proofs and programming in the same language.

Zombie is a different kind of dependently typed language, eschewing automatic β-reduction in the type checker for an approach based on explicit equality rewriting, which enables new ways of combining proofs and programs, as well as new forms of proof automation. Meanwhile, as languages designed for dependently typed programming come closer to practical applicability, Haskell is also moving towards full dependent types. We discuss the challenges and opportunities available at the cutting edge of Haskell.

In our third episode, we dicuss homotopy type theory (HoTT) with Wesleyan University’s Dan Licata. Dan has participated during much of the development of HoTT, having completed his PhD at CMU and having been a part of the Institute for Advanced Study’s special year on the subject. In our interview, we discuss the basics of HoTT, some potential applications in both mathematics and computing, as well as ongoing work on computation, univalence, and cubes.

Reading:

The HoTT book is a collaborative effort from the IAS’s Univalent Foundations program. It presents the basics of HoTT, and then demonstrates how a number of different branches of mathematics can be developed within it.

Homotopical Patch Theory by Carlo Angiuli, Edward Morehouse, Dan Licata, and Bob Harper is the expanded version of the ICFP paper mentioned in the podcast. This paper applies HoTT to a programmer-relevant topic: Darcs’s patch theory. It can serve as a good introduction to higher inductive types for those whose intuitions are based in code.

Dan’s Oxford talk: A Cubical Infinite-Dimensional Type Theory. slides / video

In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.

In our inaugural episode, we speak with Peter Dybjer from Chalmers University of Technology. Peter has made significant contributions to type theory, including inductive families, induction-recursion, and categorical models of dependent types. He is generally interested in program correctness, programming language semantics, and the connection between mathematics and programming. Today, we will talk about the relationship between QuickCheck-style testing and proofs and verification in type theory.