Constructive proofs as programs - a podcast by Aaron Stump

Constructive proofs are essentially programs; several simple examples

Further episodes of Iowa Type Theory Commute

Further podcasts by Aaron Stump

Website of Aaron Stump