Iowa Type Theory Commute

Mar 27 2025 172 ep. 13 mins 260
Iowa Type Theory Commute Podcast artwork

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

  Technology  Science
RSS feed Share
Copy RSS


Subscribe on Podcast Addict


Introduction to the Finite Developments Theorem

Mar 27 2025 15 mins  
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.

Nominal Isabelle/HOL

Jan 31 2025 16 mins  
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.

The Locally Nameless Representation

Jan 02 2025 19 mins  
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 lambd

POPLmark Reloaded, Part 2

Dec 22 2024 13 mins  
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.

POPLmark Reloaded, Part 1

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

Introduction to Formalizing Programming Languages Theory

Nov 25 2024 12 mins  
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.

Turing's proof of normalization for STLC

May 20 2024 17 mins  
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.

Introduction to normalization for STLC

May 13 2024 9 mins  
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 [email protected]).

The curious case of exponentiation in simply typed lambda calculus

May 04 2024 7 mins  
Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). But surprisingly, the type is non-uniform. If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A. The second argument needs to

Arithmetic operations in simply typed lambda calculus

May 04 2024 9 mins  
It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A. If we abbreviate that type as Nat_A, then addition and multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A.