Iowa Type Theory Commute

Hosted by Aaron Stump

Technology Science

Website RSS feed

Episodes

186

Latest episode

May 2026

Language

EN-US

About the show

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Listen to episodes

60 recent

May 7, 2026Episode 88 min

A Strange Deal, Explained

I explain the story from last episode.

May 1, 2026Episode 72 min

A Strange Deal

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.

April 20, 2026Episode 623 min

Great paper: The Calculated Typer

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

April 2, 2026Episode 513 min

Double-negation translations and CPS conversion, part 2

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.

March 31, 2026Episode 413 min

Double-negation translations and CPS conversion, part 1

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 translation: classical theorems can be translated to intuitionistic ones, by adding some double negations. As an example, we talk through the intuitionistic proof of the double negation of the law of excluded middle: not not (p or not p).

March 3, 2026Episode 322 min

What are commuting conversions in proof theory?

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 need commuting conversions to move the argument into the branches, so you can call the functions (in the then- and else-branches) with it.See Section 10.1 of Girard's Proofs and Types for more on the problem, and a nice paper by de Groote on strong normalization with commuting conversions.

January 16, 2026Episode 219 min

What is Control Flow Analysis for Lambda Calculus?

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.

November 14, 2025Episode 121 min

Measure Functions and Termination of STLC

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 this the start of season 7, because it seems about time for that.

August 22, 2025Episode 1218 min

Schematic Affine Recursion, Oh My!

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 construction"). But this prevents higher-order functions like map, which need to repeat a computation involving a variable f to be mapped over the elements of a list. The solution is to allow schematic definition of terms, using schema variables ranging over closed terms.

August 19, 2025Episode 1121 min

The Stunner: Linear System T is Diverging!

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 does not sink Victor's idea of basing type theory on a terminating untyped core language, but it does sink the specific language he and I were thinking about, namely affine lambda calculus plus structural recursion.My notes are here.