More on Computation First, and Basic Idea of Realizability - a podcast by Aaron Stump

A basic example of realizability, to show how types are defined in terms of computation

Further episodes of Iowa Type Theory Commute

Further podcasts by Aaron Stump

Website of Aaron Stump