The Iowa Type Theory Commute is a podcast aimed at a general Computer Science audience, about type theory, functional programming, formal methods, and related topics. I am organizing the podcast into chapters:

Season 1

Chapter 1: Computer-Checked Proofs and Formal Methods

Chapter 2: Functional Programming

Chapter 3: The Curry-Howard Isomorphism

Chapter 4: Programming with GADTs

Chapter 5: Type Theory Design I: Realizability

Chapter 6: Lambda Encodings

Chapter 7: Basic Metatheory for Type Theory

Chapter 8: Termination Checking

Chapter 9: Optimal Beta-Reduction

Season 2

Chapter 10: Logical Relations and Parametricity

Chapter 11: Relational Type Theory

Chapter 12: Intersection Types

The RSS URL for the podcast is .
I am experimenting with a discussion forum embedded here.

Notes on my recording setup are here.