x

75% of people globally want unbiased news (Pew Research) but are concerned they're not getting that.

Get balanced coverage with Symby. See how stories are covered across diverse outlets and spot when one side covers a story the other skips.

PODCAST

Iowa Type Theory Commute

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

technology mathematics

All Episodes

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

16:18

Nominal Isabelle/HOL

Iowa Type Theory Commute ·

2025/01/31

In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL, by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.

en-us

19:54

The Locally Nameless Representation

Iowa Type Theory Commute ·

2025/01/03

I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud. I complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction.&n...

en-us

13:59

POPLmark Reloaded, Part 2

Iowa Type Theory Commute ·

2024/12/23

I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.

en-us

15:14

POPLmark Reloaded, Part 1

Iowa Type Theory Commute ·

2024/12/23

I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations, which proposes a benchmark problem for mechanizing Programming Language theory.

en-us

12:20

Introduction to Formalizing Programming Languages Theory

Iowa Type Theory Commute ·

2024/11/25

In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers like Rocq (formerly Coq) and Agda.

en-us

17:39

Turing's proof of normalization for STLC

Iowa Type Theory Commute ·

2024/05/21

In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s. See this short note for Turing's original proof and some historical comments.

en-us

9:39

Introduction to normalization for STLC

Iowa Type Theory Commute ·

2024/05/14

In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods. We will look at proofs in more detail in the coming episodes. Feel free to join the Telegram group for the podcast if you want to discuss anything (or just email me at aaron.stump@gmail.com).

en-us

7:29

The curious case of exponentiation in simply typed...

Iowa Type Theory Commute ·

2024/05/04

en-us

183 results

Similar Podcasts

Lead With AI

Tamara Nall

Linux in the Ham Shack

Black Sparrow Media

Data Engineering Podcast

Tobias Macey

Eye On A.I.

Craig S. Smith

Reflections

Livewire Labs