Iowa Type Theory Commute
Aaron Stump
Publishing Details
About This Podcast
Explore Statistics
Recent Episodes
S7E8 A Strange Deal, Explained
I explain the story from last episode.
S7E7 A Strange Deal
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 Frank Pfenning (wearing fake horns!) at RTA in Nara,…
S7E6 Great paper: The Calculated Typer
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 at the specification of a type checker, for a very…
S7E5 Double-negation translations and CPS conversion, part 2
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…
S7E4 Double-negation translations and CPS conversion, part 1
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,…
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.
Frequently Asked Questions
Iowa Type Theory Commute has published 186 episodes since November 2019, covering topics in Mathematics, Science.
Iowa Type Theory Commute is currently moderate 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