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 https://feeds.buzzsprout.com/728558.rss .
Notes on my recording setup are here.