Iowa Type Theory Commute
Episodes
A Strange Deal, Explained
07 May 2026
Contributed by Lukas
I explain the story from last episode.
A Strange Deal
01 May 2026
Contributed by Lukas
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 Fran...
Great paper: The Calculated Typer
20 Apr 2026
Contributed by Lukas
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 a...
Double-negation translations and CPS conversion, part 2
02 Apr 2026
Contributed by Lukas
In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CPS). I sk...
Double-negation translations and CPS conversion, part 1
31 Mar 2026
Contributed by Lukas
In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming languages wh...
What are commuting conversions in proof theory?
03 Mar 2026
Contributed by Lukas
Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour...
What is Control Flow Analysis for Lambda Calculus?
16 Jan 2026
Contributed by Lukas
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 refer...
Measure Functions and Termination of STLC
14 Nov 2025
Contributed by Lukas
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 pr...
Schematic Affine Recursion, Oh My!
22 Aug 2025
Contributed by Lukas
To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-bound variab...
The Stunner: Linear System T is Diverging!
19 Aug 2025
Contributed by Lukas
In this episode, I shoot down last episode's proposal -- at least in the version I discussed -- based on an amazing observation from an astonishi...
Terminating Computation First?
01 Aug 2025
Contributed by Lukas
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,...
Correction: the Correct Author of the Proof from Last Episode, and an AI flop
12 May 2025
Contributed by Lukas
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 flop...
Krivine's Proof of FD, Using Intersection Types
05 May 2025
Contributed by Lukas
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.
A Measure-Based Proof of Finite Developments
16 Apr 2025
Contributed by Lukas
I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.
Introduction to the Finite Developments Theorem
27 Mar 2025
Contributed by Lukas
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 res...
Nominal Isabelle/HOL
31 Jan 2025
Contributed by Lukas
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-...
The Locally Nameless Representation
03 Jan 2025
Contributed by Lukas
I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written...
POPLmark Reloaded, Part 1
23 Dec 2024
Contributed by Lukas
I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations, which proposes a benchmark problem for mechanizing Programming Languag...
POPLmark Reloaded, Part 2
23 Dec 2024
Contributed by Lukas
I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga, Coq (r...
Introduction to Formalizing Programming Languages Theory
25 Nov 2024
Contributed by Lukas
In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers ...
Turing's proof of normalization for STLC
21 May 2024
Contributed by Lukas
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 or...
Introduction to normalization for STLC
14 May 2024
Contributed by Lukas
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. ...
The curious case of exponentiation in simply typed lambda calculus
04 May 2024
Contributed by Lukas
Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). But surpri...
Arithmetic operations in simply typed lambda calculus
04 May 2024
Contributed by Lukas
It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Chur...
More on basics of simple types
29 Apr 2024
Contributed by Lukas
I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
Begin Chapter on Simple Type Theory
19 Apr 2024
Contributed by Lukas
In this episode, after a pretty long hiatus, I start a new chapter on simply typed lambda calculus. I present the typing rules and give some basic e...
Some advanced examples in DCS
25 Sep 2023
Contributed by Lukas
This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird&apo...
DCS compared to termination checkers for type theories
19 Sep 2023
Contributed by Lukas
In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly...
Getting started with DCS
10 Sep 2023
Contributed by Lukas
In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here.
Introduction to DCS
04 Sep 2023
Contributed by Lukas
DCS is a new functional programming language I am designing and implementing with Stefan Monnier. DCS has a pure, terminating core, around which mon...
Semantics of subtyping
24 Jul 2023
Contributed by Lukas
I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyp...
More on type inference for simple subtypes
16 Jul 2023
Contributed by Lukas
I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.
Subtyping, the golden key
09 Jul 2023
Contributed by Lukas
In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing func...
Type inference with simple subtypes
30 Jun 2023
Contributed by Lukas
In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorith...
Basics of subtyping
21 Jun 2023
Contributed by Lukas
In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for...
Begin chapter on subtyping
21 Jun 2023
Contributed by Lukas
We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented func...
Last episode discussing Observational Equality Now for Good
13 Apr 2023
Contributed by Lukas
In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equalit...
More on observational type theory
23 Mar 2023
Contributed by Lukas
I continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the e...
Introduction to Observational Type Theory
06 Mar 2023
Contributed by Lukas
In this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier ...
Interjection: The Liquid Tensor Experiment
02 Mar 2023
Contributed by Lukas
I pause the chapter on extensionality in type theory to talk about something very exciting that I just learned about (though the project was completed...
Extensional Martin-Loef Type Theory
04 Feb 2023
Contributed by Lukas
In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that pro...
Begin chapter on extensionality
25 Jan 2023
Contributed by Lukas
This episode begins a new chapter on extensionality in type theory, where we seek to equate terms in different ways based on their types. The basic ...
Papers from Formal Methods for Blockchains 2021
01 Jan 2023
Contributed by Lukas
In this episode, I talk about two papers from the 3rd International Workshop on Formal Methods for Blockchains, 2021. Also, I am continuing my reque...
Mi-Cho-Coq: Michelson formalized and applied, in Coq
02 Dec 2022
Contributed by Lukas
In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for CertifyingTezos Smart Contracts", by Bernardo et al. The paper gives a...
Verification of Tezos smart contracts with K-Michelson
11 Nov 2022
Contributed by Lukas
In this episode (proudly wearing my "I am not an expert" hat), I discuss efforts by Runtime Verification to verify the Dexter2 defi smart co...
Start of Season 4: Formal Methods for Blockchain
07 Nov 2022
Contributed by Lukas
I start off a new chapter (seventeen!) of the podcast, to talk about formal methods for blockchain systems. In the next few episodes, we will look a...
Separation Logic II: recursive predicates
16 Sep 2022
Contributed by Lukas
I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds. An important idea is describing data structure u...
Separation Logic 1
25 Jul 2022
Contributed by Lukas
I discuss separation logic, as presented in this seminal paper by the great John C. Reynolds. I did not go very far into the topic, so please expect...
Let's talk about Rust
10 Jul 2022
Contributed by Lukas
In this episode, I talk briefly about Rust, which uses compile-time analysis to ensure that code is memory-safe (and also free of data races in concur...
Region-Based Memory Management
22 Jun 2022
Contributed by Lukas
I discuss the idea of statically typed region-based memory management, proposed by Tofte and Talpin. The idea is to allow programmers to declare exp...
Introduction to verified memory management
05 Jun 2022
Contributed by Lukas
In this episode, I start a new chapter (we are up to Chapter 16, here), about verifying safe manual management of memory. I have personally gotten p...
More on Metamath
21 May 2022
Contributed by Lukas
I laud the Metamath proof checker and its excellent book. I am also looking for suggestions on what to discuss next, as I am ready to wrap up this c...
Metamath
23 Apr 2022
Contributed by Lukas
In this episode I share my initial impressions -- very positive! -- of the Metamath system. Metamath allows one to develop theorems from axioms whic...
The Seventeen Provers of the World
10 Apr 2022
Contributed by Lukas
I discuss a book edited by Freek Wiedijk (pronounced "Frake Weedike"), which describes the solutions he received in response to a call for f...
More on Lean
13 Mar 2022
Contributed by Lukas
I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.
The Lean Prover
28 Feb 2022
Contributed by Lukas
In this episode, I talk about what I have learned so far about the Lean prover, especially from an excellent (if somewhat advanced) Master's thes...
More on Isabelle, and the Complexity of ITPs
17 Feb 2022
Contributed by Lukas
I talk about my attempts to use Isabelle as a newbie, and reflect a little on the complexity of both Isabelle and Coq.
Isabelle/HOL
28 Jan 2022
Contributed by Lukas
The Isabelle theorem prover supports different logics, but its most developed seems to be Higher-Order Logic (HOL). In this episode, I talk about th...
More on Agda
13 Jan 2022
Contributed by Lukas
I talk a bit more about the Agda proof assistant.
A look at Agda
10 Jan 2022
Contributed by Lukas
In this episode I talk a bit about the Agda proof assistant.
More reflections on Coq
31 Dec 2021
Contributed by Lukas
I talk about a couple good resources for learning Coq, the problem of too many ways to do things in type theory, and issues trying to explain and docu...
The Coq Proof Assistant
29 Dec 2021
Contributed by Lukas
I discuss Coq, a widely used proof assistant based on a constructive type theory. One episode definitely cannot do justice to the complexity of a to...
Introduction to Interactive Theorem Provers
17 Dec 2021
Contributed by Lukas
This is the start of Chapter 15, about interactive theorem provers (ITPs). In this episode, I talk about the difference between fully automatic and ...
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
11 Dec 2021
Contributed by Lukas
In this episode, I outline the argument for why the proof-theoretic ordinal (in the sense of Rathjen, as presented last episode) is epsilon-0. My ex...
The proof-theoretic ordinal of a logical theory
21 Nov 2021
Contributed by Lukas
Ordinal analysis seeks to determine the strength of a logical theory by assigning an ordinal to it. Which one? In this episode I describe a defini...
Introduction to Ordinal Analysis
17 Nov 2021
Contributed by Lukas
Ordinal analysis is an important branch of proof theory, which seeks to compare, quantitatively, the strengths of different proof systems. The quant...
An analogy for multiplicative disjunction
03 Nov 2021
Contributed by Lukas
Listen in while I have an actual insight on air! After a week of head scratching, I figure out -- while chattering! -- what I hope is both a correct...
Linear conjunctions and disjunctions
29 Oct 2021
Contributed by Lukas
I explain the basic idea of multiplicative versus additive proof rules, and consider multiplicative conjunction (tensor), addition conjunction (&,...
A taste of linear logic
22 Oct 2021
Contributed by Lukas
We discuss briefly the central ideas of linear logic, where by default assumptions must be used exactly once.
Structural rules, or the Curse of the Bound Variable
13 Oct 2021
Contributed by Lukas
In this episode I discuss the basic structural rules of weakening, contraction, and exchange, and speculate on their dark origin.
Why Cut Elimination is More Complicated than Normalization
05 Oct 2021
Contributed by Lukas
Cut elimination for sequent calculus is more involved that normalization of detours for natural deduction. There are more cases of cuts that must be...
Introduction to Cut Elimination
29 Sep 2021
Contributed by Lukas
We saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is ...
Normalization of detours for implication inferences
19 Sep 2021
Contributed by Lukas
We talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implicati...
Normalization in natural deduction
18 Sep 2021
Contributed by Lukas
This episode explains the idea of normalization of proofs in natural deduction. We want to eliminate so-called detours in proofs, which occur when a...
A Brief Look at Sequent Calculus
16 Sep 2021
Contributed by Lukas
Sequent calculus is a different style in which proof systems can be formulated, where for each connective, we have a left rule for introducing it (in ...
Implication rules for natural deduction
14 Sep 2021
Contributed by Lukas
We discuss further inferences in natural deduction, in particular implication introduction and elimination.
Natural deduction: or, the bad news!
14 Sep 2021
Contributed by Lukas
We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences. It is...
Natural Deduction
12 Sep 2021
Contributed by Lukas
This episode begins the discussion of the style of proof known as Natural Deduction, invented by Gerhard Gentzen, a student of Hermann Weyl, himself a...
Rules of proof, standard proof systems
09 Sep 2021
Contributed by Lukas
We continue our gradual entry into proof theory by talking about reflecting meta-logical reasoning into logical rules, and naming the three basic proo...
Different proof systems, distinguishing logical rules from domain axioms
02 Sep 2021
Contributed by Lukas
I highlight two basic points in this continuing warm-up to proof theory: there are different proof systems for the same logics, and it is customary to...
Introduction to Proof Theory (Start of Season 3)
31 Aug 2021
Contributed by Lukas
This is the start of Season 3 of the podcast. We are beginning with a new chapter (Chapter 14) on Proof Theory. This episode gives some basic in...
Modula-2
28 Jul 2021
Contributed by Lukas
In this episode I discuss the paper "Modula-2 and Oberon" by Niklaus Wirth. Modula-2 introduced (it seems from the paper) the idea of havi...
Decomposing recursions using algebras
13 Jul 2021
Contributed by Lukas
Analogously to the decomposition of a datatype into a functor (which can be built from other functors to assemble a bigger language from smaller piece...
Reassembling datatypes from functors using a fixed-point
11 Jul 2021
Contributed by Lukas
Last episode we discussed how functors can describe a single level of a datatype. In this episode, we discuss how to put these functors back togethe...
Decomposing datatypes into functors
03 Jul 2021
Contributed by Lukas
This episode continues the discussion of Swierstra's paper "Datatypes à la Carte", explaining how we can decompose a datatype into the...
Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte"
24 Jun 2021
Contributed by Lukas
In a really wonderful paper of some few years back, Swierstra introduced the idea of modular datatypes using ideas from universal algebra. Modular d...
Modules for Mathematical Theories (MMT)
09 Jun 2021
Contributed by Lukas
In a 2013 journal article titled "A Scalable Module System", Florian Rabe and Michael Kohlhase propose a module system called MMT (Modules f...
Some thoughts on module systems so far
19 May 2021
Contributed by Lukas
I look back at the module systems we considered so far (Haskell's, Standard ML's, and Agda's), and consider a few points that are on my...
A look at Agda's module system
12 May 2021
Contributed by Lukas
Agda's module system (beautifully described here) could be seen as intermediate between Haskell's and Standard ML's. It supports nest...
Standard ML: the Newmar King-Aire of module systems
10 May 2021
Contributed by Lukas
SML has arguably the most complicated/powerful module system of any existing programming language. It is a luxury RV to Haskell's camper van. ...
A look at Haskell's module system
27 Apr 2021
Contributed by Lukas
I briefly survey the main features of Haskell's module system, and reflect a bit on its design.
Let's talk about modules!
20 Apr 2021
Contributed by Lukas
I start Chapter 13 (in Season 2) of the podcast, on module systems. Almost all programming languages I know include some kind of scheme for modules,...
Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation
12 Apr 2021
Contributed by Lukas
I was reading Benjamin Pierce's dissertation, and learning some intriguing things about intersection types in the context of Church-style typing....
Intersections and Unions in Practice; Failure of Type Preservation with Unions
22 Mar 2021
Contributed by Lukas
I discuss the perhaps surprising fact that union and intersection types are quite actively used and promoted for languages like TypeScript, also OO la...
Normal terms are typable with intersection types
05 Mar 2021
Contributed by Lukas
I sketch the argument that pure lambda terms in normal form are typable using intersection types. This completes the argument started in the previou...
Intersection Types Preserved Under Beta-Expansion
15 Feb 2021
Contributed by Lukas
Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable. So typing is clo...
Introduction to Intersection Types
09 Feb 2021
Contributed by Lukas
In a type system with intersection types, a term t that has type A and also has type B can be assigned the type 'A intersect B'. This epi...
Deriving disjointness of constructor ranges in RelTT
02 Feb 2021
Contributed by Lukas
Responding to an email question from a listener, I explain how to derive a form of inconsistency from the assumption that True is related to False at ...
Software Design and Intrinsic Identity
21 Jan 2021
Contributed by Lukas
I muse about the hopeless prospect of a single intrinsic conceptual decomposition of a problem domain in software engineering, and relate this to the ...
Identity Inclusion in Relational Type Theory
18 Jan 2021
Contributed by Lukas
Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "T...