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 .

You can listen to The Stunner: Linear System T is Diverging! online on Radio and Podcast. Open the player on this page to stream the available audio.

The Stunner: Linear System T is Diverging! is an episode from Iowa Type Theory Commute by Aaron Stump.

This episode is 21:03 long.

This episode was published on Aug 19, 2025.

Yes. Use the heart button on the episode page to add it to your favorite episodes list.

Yes. This page shows related episodes from Iowa Type Theory Commute when more episodes are available from the podcast feed.