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...

April 18, 2015 n/a

Episode 3: Dan Licata on Homotopy Type Theory

January 7, 2015 n/a

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.

September 26, 2014 1h32m

Episode 1: Peter Dybjer on types and testing

We speak with Peter Dybjer about the relationship between QuickCheck-style testing and proofs and verification in type theory.

August 13, 2014 n/a