Curry-Howard for classical logic - a podcast by Aaron Stump

Amazingly, nonconstructive proofs can also be given a computational interpretation, using control operators

Further episodes of Iowa Type Theory Commute

Further podcasts by Aaron Stump

Website of Aaron Stump