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:

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


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.