Iowa Type Theory Commute

14:25

Autoformalization of Fermat's Last Theorem

Iowa Type Theory Commute ·

2026/09/15

In this episode, I reflect on the recent announcement that Anthropic researchers have autoformalized the proof of Fermat's Last Theorem. That is, they instructed an LLM to create a computer-checkable proof, in the Lean prover, of this theorem, following existing paper proofs in the literature. The resulting proof weighs in at 13 million lines of Lean, a staggering amount.

en-us

20:09

A Fireball of Alpha

Iowa Type Theory Commute ·

2026/08/21

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 state and prove theorems about alpha-equivalence. One example class of such theorems concern when alpha-equivalence can be avoided, in the sense that beta-reduction can proceed without any variable capture, while not requiring renaming variables. I have a compan...

en-us

22:45

Solving Quadratic Word Equations

Iowa Type Theory Commute ·

2026/08/11

A system of word equations is called quadratic if no variable occurs more than twice in it. There is an interesting simple algorithm to solve quadratic systems of word equations, which I talk through in this episode. My source is Chapter 12 of "Algebraic Combinatorics on Words" by Lothaire.

en-us

17:14

A little bit about word equations

Iowa Type Theory Commute ·

2026/08/03

The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tenth problem. Word equations relate expressions consisting of concatenations of variables and constant symbols. An example is a X = X a, where X is a variable and a is a constant. A solution maps variables to strings of constant symbols making the two sides identical. In this episode, I discuss the problem a little, and what I learned so far about how it is solved.

en-us

20:30

Coercive subtyping and coherence

Iowa Type Theory Commute ·

2026/07/01

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering perspective. I also explain the critical concept of coherence.

en-us

8:23

A Strange Deal, Explained

Iowa Type Theory Commute ·

2026/05/07

I explain the story from last episode.

en-us

2:57

A Strange Deal

Iowa Type Theory Commute ·

2026/05/01

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 my take on it. In a subsequent episode, I will explain how the story illustrates the computational interpretation of the law of excluded middle.

en-us

23:41

Great paper: The Calculated Typer

Iowa Type Theory Commute ·

2026/04/20

I discuss a nice paper I quite enjoyed reading, called The Calculated Typer, by Garby, Bahr, and Hutton. The authors take a very nice general look at the specification of a type checker, for a very simple expression language. They then manually derive the actual code for the type checker by effectively trying to prove that this as yet unknown code satisfies its spec. (This is what is meant by calculating the type checker.)

en-us

13:31

Double-negation translations and CPS conversion, part 2

Iowa Type Theory Commute ·

2026/04/02

In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CPS). I sketch how CPS conversion (transforming a program with callcc into one in CPS that does not need callcc any more) corresponds to double-negation translation from classical to intuitionistic logic. The paper I am referencing is here.

en-us

13:48

Double-negation translations and CPS conversion, part 1

Iowa Type Theory Commute ·

2026/03/31

In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming languages where formulas in logic are identified with types, and proofs with programs). This is the identification of double-negation translations in logic, which go back to a paper of Kolmogorov's in 1925, with conversion to continuation-passing style (CPS), a compilation technique. For this episode, we just discuss the idea of double-negation ...

en-us

22:29

What are commuting conversions in proof theory?

Iowa Type Theory Commute ·

2026/03/03

Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled. The stuck inferences are uses of disjunction elimination. In programming terms, if you have an if-then-else (a simple case of or-elimination) where the then- and else-branches are lambda abstractions, and you apply that if-then-else to an argument, you n...

en-us

19:24

What is Control Flow Analysis for Lambda Calculus?

Iowa Type Theory Commute ·

2026/01/16

I am currently on a frolic into the literature on Control Flow Analysis (CFA), and discuss what this is, for pure lambda calculus. A wonderful reference for this is this paper by Palsberg.

en-us

21:42

Measure Functions and Termination of STLC

Iowa Type Theory Commute ·

2025/11/14

In this episode, I talk about what we should consider to be a measure function. Such functions can be used to show termination of some process or program, by assigning a measure to each program, and showing that as the program computes, the measure decreases in some well-founded ordering. But what should count as a measure function? The context for this is RTA Open Problem 19, on showing termination for the simply typed lambda calculus using a measure function. Let's call th...

en-us

18:49

Schematic Affine Recursion, Oh My!

Iowa Type Theory Commute ·

2025/08/22

To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-bound variables are used at most once) plus structural recursion does not enforce termination, even if you restrict the recursor so that the function to be iterated is closed when you reduce ("closed at reduction"). You have to restrict it so that recursion terms are disallowed entirely unless the function to be iterated is closed ("closed at cons...

en-us

21:03

The Stunner: Linear System T is Diverging!

Iowa Type Theory Commute ·

2025/08/19

In this episode, I shoot down last episode's proposal -- at least in the version I discussed -- based on an amazing observation from an astonishing paper, "Gödel’s system T revisited", by Alves, Fernández, Florido, and Mackie. Linear System T is diverging, as they reveal through a short but clever example. It is even diverging if one requires that the iterator can only be reduced when the function to be iterated is closed (no free variables). This extraordinary observation d...

en-us

11:27

Terminating Computation First?

Iowa Type Theory Commute ·

2025/08/01

In this episode, I discuss an intriguing idea proposed by Victor Taelin, to base a logically sound type theory on an untyped but terminating language, upon which one may then erect as exotic a type system as one wishes. By enforcing termination already for the untyped language, we no longer have to make the type system do the heavy work of enforcing termination.

en-us

7:10

Correction: the Correct Author of the Proof from Last...

Iowa Type Theory Commute ·

2025/05/12

I correct what I said in the last episode about the author of the proof of FD from last episode based on intersection types. I also describe AI flopping when I ask it a question about this.

en-us

21:35

Krivine's Proof of FD, Using Intersection Types

Iowa Type Theory Commute ·

2025/05/05

Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types. I discuss this proof in this episode.

en-us

23:24

A Measure-Based Proof of Finite Developments

Iowa Type Theory Commute ·

2025/04/16

I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.

en-us

15:54

Introduction to the Finite Developments Theorem

Iowa Type Theory Commute ·

2025/03/27

The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate. In this episode, I discuss the theorem and why I got interested in it.

en-us

All Episodes

Similar Podcasts

Lead With AI

Tamara Nall

Elon Musk Podcast

Stage Zero

Modem Futura

Sean Leahy, Andrew Maynard

Cisco Podcast Network

Cisco

MSP Business School

MSP Business School