A Strange Deal

Iowa Type Theory Commute by Aaron Stump

Apr 30, 20262:57Technology

The Curry-Howard isomorphism for the law of excluded middle, as a radio drama. I first saw a version of this story performed by Phil Wadler and Frank Pfenning (wearing fake horns!) at RTA in Nara, Japan in 2005. This is...

Related Episodes

Continue listening to more episodes from Iowa Type Theory Commute.

Autoformalization of Fermat's Last Theorem

Sep 15, 2026 - 14:25

In this episode, I reflect on the recent announcement that Anthropic researchers have autoformalized the...

A Fireball of Alpha

Aug 21, 2026 - 20:09

I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence,...

Solving Quadratic Word Equations

Aug 11, 2026 - 22:45

A system of word equations is called quadratic if no variable occurs more than twice in it. There is an i...

A little bit about word equations

Aug 3, 2026 - 17:14

The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tent...

Coercive subtyping and coherence

Jul 1, 2026 - 20:30

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering pers...

A Strange Deal, Explained

May 7, 2026 - 8:23

I explain the story from last episode.

Great paper: The Calculated Typer

Apr 20, 2026 - 23:41

I discuss a nice paper I quite enjoyed reading, called The Calculated Typer , by Garby, Bahr, and Hutton....

Double-negation translations and CPS conversion, part 2

Apr 2, 2026 - 13:31

In this episode, I talk about the control operator callcc, and how it is implemented during compilation u...