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 https://feeds.buzzsprout.com/728558.rss .
I am experimenting with a discussion forum embedded here.
Notes on my recording setup are here.