Publishing Details
About This Podcast
Explore Statistics
Recent Episodes
S7E3 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…
S7E2 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.
S7E1 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…
S6E12 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…
S6E11 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,…
S6E10 Terminating Computation First?
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…
S6E9 Correction: the Correct Author of the Proof from Last Episode, and an AI flop
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.
S6E8 Krivine's Proof of FD, Using Intersection Types
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.
S6E7 A Measure-Based Proof of Finite Developments
I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.
S6E6 Introduction to the Finite Developments Theorem
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…
S6E5 Nominal Isabelle/HOL
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…
S6E4 The Locally Nameless Representation
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…
S6E3 POPLmark Reloaded, Part 2
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.
S6E2 POPLmark Reloaded, Part 1
I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations, which proposes a benchmark problem for mechanizing Programming Language theory.
S6E1 Introduction to Formalizing Programming Languages Theory
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.
S5E6 Turing's proof of normalization for STLC
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.
S5E5 Introduction to normalization for STLC
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…
S5E4 The curious case of exponentiation in simply typed lambda calculus
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…
S5E3 Arithmetic operations in simply typed lambda calculus
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…
S5E2 More on basics of simple types
I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
Frequently Asked Questions
Iowa Type Theory Commute has published 181 episodes since November 2019, covering topics in Mathematics, Science.
Iowa Type Theory Commute is currently highly active with new episodes every 2 weeks. Average episode length is 13m.
Similar Podcasts
19 Keys Presents High Level Conversations
EYL Network
484 episodes
Data Skeptic
Kyle Polich
601 episodes
Zero Knowledge
Zero Knowledge Podcast
414 episodes
Data Science Leaders
Domino Data Lab
100 episodes
Data Driven
Data Driven
300 episodes
The AI with Maribel Lopez (AI with ML)
Maribel Lopez
78 episodes