Best Finite Languages Podcasts (2025)

1
Correction: the Correct Author of the Proof from Last Episode, and an AI flop 7:10

Play Pause

2M ago7:10

7:10

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.By Aaron Stump

1
Krivine's Proof of FD, Using Intersection Types 21:35

3M ago21:35

21:35

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.By Aaron Stump

1
A Measure-Based Proof of Finite Developments 23:24

3M ago23:24

23:24

I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.By Aaron Stump

1
Introduction to the Finite Developments Theorem 15:54

4M ago15:54

15:54

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.…

1
Nominal Isabelle/HOL 16:18

6M ago16:18

16:18

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.By Aaron Stump

1
The Locally Nameless Representation 19:54

7M ago19:54

19:54

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 t…

1
POPLmark Reloaded, Part 1 15:14

7M ago15:14

15:14

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

1
POPLmark Reloaded, Part 2 13:59

7M ago13:59

13:59

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.By Aaron Stump

1
Introduction to Formalizing Programming Languages Theory 12:20

8M ago12:20

12:20

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.By Aaron Stump

1
Turing's proof of normalization for STLC 17:39

1y ago17:39

17:39

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.By Aaron Stump

1
Introduction to normalization for STLC 9:39

1y ago9:39

9:39

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]).…

1
Arithmetic operations in simply typed lambda calculus 9:56

1y ago9:56

9:56

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 …

1
The curious case of exponentiation in simply typed lambda calculus 7:29

1y ago7:29

7:29

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 a…

1
More on basics of simple types 15:45

1y ago15:45

15:45

I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.By Aaron Stump

1
Begin Chapter on Simple Type Theory 15:41

1+ y ago15:41

15:41

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 examples. Subsequent episodes will discuss various interesting nuances...By Aaron Stump

1
Some advanced examples in DCS 23:16

2y ago23:16

23:16

This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time. I explain these examples in detail and then discuss how they are implemented in DCS, which ensur…

1
DCS compared to termination checkers for type theories 19:45

2y ago19:45

19:45

In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here.By Aaron Stump

1
Getting started with DCS 17:23

2y ago17:23

17:23

In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here.By Aaron Stump

1
Introduction to DCS 11:36

2y ago11:36

11:36

DCS is a new functional programming language I am designing and implementing with Stefan Monnier. DCS has a pure, terminating core, around which monads will be layered for possibly diverging, impure computation. In this episode, I talk about this basic design, and its rationale.By Aaron Stump

1
Semantics of subtyping 15:20

2y ago15:20

15:20

I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping. The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a comparison of the two kinds of subtyping. With coercive subtyping, we have subtyping axioms "A

1
More on type inference for simple subtypes 9:06

2y ago9:06

9:06

I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.By Aaron Stump

1
Subtyping, the golden key 9:13

2y ago9:13

9:13

In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing functional programmers to drop various irritating function calls that are needed just to make types work out. Examples are lifting functions with monad transformers, or even just the pure/return functions…

1
Type inference with simple subtypes 13:27

2y ago13:27

13:27

In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus. I mostly focus here on how subtype constraints allow typing any term (which seems surprising). You can join the tel…

1
Basics of subtyping 8:05

2y ago8:05

8:05

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 arrow types.By Aaron Stump

1
Begin chapter on subtyping 16:15

2y ago16:15

16:15

We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very useful for writing lighter, more elegant code. I also talk about how subtyping could help realize a new vision …

1
Last episode discussing Observational Equality Now for Good 12:15

2+ y ago12:15

12:15

In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equality -- Now for Good!". I talk a bit about the structure of the normalization proof in the paper, which uses induction recursion. See this paper by Peter Dybjer for more about that feature. Also, feel free to join…

1
More on observational type theory 13:43

2+ y ago13:43

13:43

I continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality type), and how proofs of equalities can be used to cast terms from one type to another. Also, in exciting…

1
Introduction to Observational Type Theory 10:10

2+ y ago10:10

10:10

In this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier work of McBride, Swierstra, and Altenkirch (which I will cover in a later episode) on a new approach to making a type theory extensional. The idea is to have equality types reduce, within the theory, to stateme…

1
Interjection: The Liquid Tensor Experiment 12:24

2+ y ago12:24

12:24

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 Summer 2022): the so-called Liquid Tensor Experiment, to formalize a recent very difficult proof by a mathematician named Peter Scholze, in Lean. This is the first time in history, that I know of, wh…

1
Extensional Martin-Loef Type Theory 11:23

2+ y ago11:23

11:23

In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that propositional equality implies definitional equality. Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitional…

1
Begin chapter on extensionality 10:27

2+ y ago10:27

10:27

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 example is function extensionality, where we would like to equate functions from A to B if given equal inputs at type A, they produce equal outputs at type B. With this definition, quicksort and mergeso…

1
Papers from Formal Methods for Blockchains 2021 17:01

2+ y ago17:01

17:01

In this episode, I talk about two papers from the 3rd International Workshop on Formal Methods for Blockchains, 2021. Also, I am continuing my request for your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout. To donate, click here, and then under "Gift details" select "Search for additional options" and the…

1
Mi-Cho-Coq: Michelson formalized and applied, in Coq 15:34

2+ y ago15:34

15:34

In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts", by Bernardo et al. The paper gives a nice and very clear introduction to the Michelson language, and a formalization of it in Coq. This is used to prove a correctness property about a Multisig contract. I also kindly solicit your small donations (…

1
Verification of Tezos smart contracts with K-Michelson 14:24

2+ y ago14:24

14:24

In this episode (proudly wearing my "I am not an expert" hat), I discuss efforts by Runtime Verification to verify the Dexter2 defi smart contract, using their K-Michelson tool, which provides an executable description of the operational semantics of the Michelson language used for smart contracts on the Tezos blockchain.…

1
Start of Season 4: Formal Methods for Blockchain 10:58

2+ y ago10:58

10:58

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 at some verification efforts related to the Tezos blockchain.By Aaron Stump

1
Separation Logic II: recursive predicates 11:52

3y ago11:52

11:52

I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds. An important idea is describing data structure using separating conjunction and recursive predicates.By Aaron Stump

1
Separation Logic 1 13:26

3y ago13:26

13:26

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 a follow-up episode.By Aaron Stump

1
Let's talk about Rust 13:47

3y ago13:47

13:47

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 concurrent code) without using a garbage collector. Fantastic! The language draws on but richly develops ideas on ownership that originated in academic research.…

1
Region-Based Memory Management 16:57

3y ago16:57

16:57

I discuss the idea of statically typed region-based memory management, proposed by Tofte and Talpin. The idea is to allow programmers to declare explicitly the region from which to satisfy individual allocation requests. Regions are created in a statically scoped way, so that after execution leaves the body of the region-creation construct, the ent…

1
Introduction to verified memory management 17:08

3y ago17:08

17:08

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 pretty interested in this topic, having seen through some simple experiments with Haskell how much time can go into garbage collection for seemingly simple benchmarks. I also talk about why verifying mem…

1
More on Metamath 17:19

3y ago17:19

17:19

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 chapter on proof assistants.By Aaron Stump

1
Metamath 14:32

3y ago14:32

14:32

In this episode I share my initial impressions -- very positive! -- of the Metamath system. Metamath allows one to develop theorems from axioms which you state. Typing or other syntactic requirements of axioms or theorems are also expressed axiomatically. The system exhibits an elegant coherent vision for how such a tool should work, and was super …

1
The Seventeen Provers of the World 10:36

3+ y ago10:36

10:36

I discuss a book edited by Freek Wiedijk (pronounced "Frake Weedike"), which describes the solutions he received in response to a call for formalized proofs of the irrationality of the square root of 2. The book was published in 2006, and made an impression on me then. The provers we have discussed so far all have a solution in the book, except for…

1
More on Lean 15:17

3+ y ago15:17

15:17

I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.By Aaron Stump

1
The Lean Prover 14:52

3+ y ago14:52

14:52

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 thesis, "The Type Theory of Lean" by Marco Garneiro.By Aaron Stump

1
More on Isabelle, and the Complexity of ITPs 16:14

3+ y ago16:14

16:14

I talk about my attempts to use Isabelle as a newbie, and reflect a little on the complexity of both Isabelle and Coq.By Aaron Stump

1
Isabelle/HOL 16:54

3+ y ago16:54

16:54

The Isabelle theorem prover supports different logics, but its most developed seems to be Higher-Order Logic (HOL). In this episode, I talk about the logic and approach of Isabelle/HOL, as far as I have understood them.By Aaron Stump

1
More on Agda 13:03

3+ y ago13:03

13:03

I talk a bit more about the Agda proof assistant.By Aaron Stump

1
A look at Agda 15:24

3+ y ago15:24

15:24

In this episode I talk a bit about the Agda proof assistant.By Aaron Stump

1
More reflections on Coq 18:28

3+ y ago18:28

18:28

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 document a very complex language.By Aaron Stump