A Fireball of Alpha

Iowa Type Theory Commute by Aaron Stump

Aug 21, 202620:09Technology

I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church. One reason to do that, besides just a love of being ornery, is to be able to sta...

Related Episodes

Continue listening to more episodes from Iowa Type Theory Commute.

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.

A Strange Deal

Apr 30, 2026 - 2:57

The Curry-Howard isomorphism for the law of excluded middle, as a radio drama. I first saw a version of t...

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...

Double-negation translations and CPS conversion, part 1

Mar 31, 2026 - 13:48

In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connecti...