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 (2019-2020)

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 (2020-2021)

Chapter 10: Logical Relations and Parametricity

Chapter 11: Relational Type Theory

Chapter 12: Intersection Types

Chapter 13: Module Systems

Season 3 (2021-2022)

Chapter 14: Proof Theory

Chapter 15: Proof Assistants

Season 4 (2022-2023)

Chapter 16: Verified Memory Management

Chapter 17: Formal Methods for Blockchain

Chapter 18: Extensionality in Type Theory

Chapter 19: Subtyping

Chapter 20: DCS

The RSS URL for the podcast is .

Notes on my recording setup are here.