The Type Theory Podcast

Follow The Type Theory Podcast
Share on
Copy link to clipboard

We interview experts and researchers in type theory, from the perspectives of programming, mathematics, and philosophy.

The Type Theory Podcast


    • Dec 1, 2016 LATEST EPISODE
    • infrequent NEW EPISODES
    • 1h 32m AVG DURATION
    • 6 EPISODES


    Search for episodes from The Type Theory Podcast with a specific topic:

    Latest episodes from The Type Theory Podcast

    Episode 6: Aaron Stump on Cedille

    Play Episode Listen Later Dec 1, 2016


    Episode 6: Aaron Stump on Cedille

    Episode 5: Bob Constable on CTT and Nuprl

    Play Episode Listen Later Aug 31, 2015


    Episode 5: Bob Constable on CTT and Nuprl

    Episode 4: Stephanie Weirich on Zombie and Dependent Haskell

    Play Episode Listen Later Apr 18, 2015


    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.

    Episode 3: Dan Licata on Homotopy Type Theory

    Play Episode Listen Later Jan 7, 2015


    Episode 3: Dan Licata on Homotopy Type Theory

    Episode 2: Edwin Brady on Idris

    Play Episode Listen Later Sep 26, 2014 92:50


    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 1: Peter Dybjer on types and testing

    Play Episode Listen Later Aug 13, 2014


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

    Claim The Type Theory Podcast

    In order to claim this podcast we'll send an email to with a verification link. Simply click the link and you will be able to edit tags, request a refresh, and other features to take control of your podcast page!

    Claim Cancel