From the about page:
The Type Theory Podcast is a podcast about type theory and its interactions with programming, mathematics, and philosophy. Our goal is to bring interesting research to a wider audience.
I’m not sure how I missed this when it started. 😉
There are three episodes available now:
Episode 1: Peter Dybjer on types and testing
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.
Episode 2: Edwin Brady on Idris
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.
Episode 3: Dan Licata on Homotopy Type Theory
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.
Each episode has links to additional reading materials and resources.
Enjoy!