Best Finite Languages Podcasts (2025)

1
Schematic Affine Recursion, Oh My! 18:49

Play Pause

2M ago18:49

18:49

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 recursion does not enforce termination, even if you restrict the recursor so that the function to be iterated is closed when you reduce ("closed at reduction")…

1
The Stunner: Linear System T is Diverging! 21:03

2M ago21:03

21:03

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, Fernández, Florido, and Mackie. Linear System T is diverging, as they reveal through a short but clever example. It is even diverging if one requires that …

1
Eigenvalues and Eigenvectors: The Secret Sauce of Modern Tech (From Graphics to Google) 18:06

2M ago18:06

18:06

This episode outlines Eigenvalues and Eigenvectors in Linear Algebra. We highlight the practical uses of these abstract topics.By AmCan Tech

1
Decoding Language: The Power of Context-Free Grammars in Computing 17:07

2M ago17:07

17:07

This bonus episode explores what context-free grammars are in automata theorem.By AmCan Tech

1
Demystifying Automata Theory: From Finite Machines to Regular Languages 1:03:36

3M ago1:03:36

1:03:36

This deep dive offers comprehensive overview of automata theory and formal languages. They begin by introducing finite automata (FA), including Deterministic Finite Automata (DFA) and Non-deterministic Finite Automata (NFA), alongside fundamental concepts like alphabets, strings, and languages, and their associated operations.…

1
Terminating Computation First? 11:27

3M ago11:27

11:27

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 system as one wishes. By enforcing termination already for the untyped language, we no longer have to make the type system do the heavy work of enforcin…

1
Secrets Hidden in PDF Pages 17:50

5M ago17:50

17:50

In this episode, we explore a novel method for distributed steganography using PDF files. The technique involves splitting a secret message using secret sharing algorithms and embedding the parts into PDFs by manipulating their internal structure—specifically through hidden pages. We discuss how this approach makes the embedded data virtually invis…

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

6M 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

6M 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

6M 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
Finite Automata - What you need to know 26:13

7M ago26:13

26:13

Automata theory: it's a computational model study, focusing on finite automata (DFA and NFA) and push-down automata (PDA). The course explores regular languages, their properties and proofs of non-regularity using concepts like the pumping lemma and Myhill-Nerode theorem. Foundational mathematical concepts such as set theory, sequences, relations, …

1
Shamir's Secret: A PayPal Near-Disaster 8:21

7M ago8:21

8:21

This account recounts a nightmarish incident at PayPal where a flawed implementation of Shamir Secret Sharing, a cryptographic technique for distributing a secret key among multiple parties, nearly caused a catastrophic system failure. The author, a PayPal engineer, explains the process of Shamir Secret Sharing and how he implemented it to improve …

1
Introduction to the Finite Developments Theorem 15:54

7M 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
SLAP and FLOP: Apple Silicon Speculative Execution Attacks 15:33

7M ago15:33

15:33

SLAP and FLOP are two new speculative execution attacks targeting Apple's M-series chips. SLAP exploits the Load Address Predictor (LAP) to leak data by predicting incorrect memory addresses, while FLOP leverages the Load Value Predictor (LVP) to predict incorrect data values. Both attacks allow unauthorized access to sensitive information from web…

1
Subaru Starlink Security Flaw 10:51

8M ago10:51

10:51

Security researchers discovered and exploited a vulnerability in Subaru's Starlink connected car system. This flaw allowed unauthorized access to sensitive data, including vehicle location history, and control over features like door locks. The vulnerability stemmed from weaknesses in the Starlink admin panel, which was accessible using readily ava…

1
Hash Tables: Theory, Implementation, and Universal Hashing 16:14

8M ago16:14

16:14

In this episode, we explore hash tables, a data structure designed for efficient insertion, deletion, and searching of data using keys. The document contrasts direct addressing with hashing, highlighting the space efficiency of hash tables when dealing with large key universes. It discusses collision resolution techniques like chaining and open add…

1
Suffix Trees: Construction, Properties, and Applications 9:53

9M ago9:53

9:53

Today, we are exploring suffix trees, a data structure used for solving string problems.We begin with basic definitions related to strings and alphabets, then introduces suffix trees as compressed tries containing all suffixes of a given text. Applications include substring searching, finding repeated substrings, and data compression. The discussio…

1
Disjoint Sets: Data Structures and Algorithms 12:09

9M ago12:09

12:09

We discuss disjoint sets, also known as union-find data structures. Disjoint sets maintain collections of elements partitioned into non-overlapping sets, each with a representative element. Key operations include Make-Set (creating a new set), Find-Set (locating a set's representative), and Union (merging two sets). Different representations are ex…

1
B-Tree Data Structure: Search, Insertion, and Deletion 17:53

9M ago17:53

17:53

Jump in and discover the B-tree data structure, a fundamental tool for processing queries on one-dimensional data stored on disk. We explain how B-trees efficiently support range reporting, successor/predecessor searches, insertion, and deletion operations.By AmCan Tech

1
Nominal Isabelle/HOL 16:18

9M 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
Tries: Data Structures for String Processing 15:45

9M ago15:45

15:45

A Trie, also known as a prefix tree, is a specialized tree-based data structure primarily used for efficiently storing and retrieving strings. Unlike traditional search trees where a node stores the entire key, each node in a trie represents a prefix shared by all its descendants. This unique structure facilitates fast search, insertion, and deleti…

1
Topological Sort and Strongly Connected Components 14:04

9M ago14:04

14:04

This podcast reviews key concepts related to Depth First Search (DFS) algorithm and its application in topological sorting and finding strongly connected components in graphs.By AmCan Tech

1
The Locally Nameless Representation 19:54

10M 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

10M 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

10M 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
QuickSort and Order Selection 14:08

10M ago14:08

14:08

This episode focuses on QuickSort, a divide-and-conquer sorting algorithm, comparing it to MergeSort, and analyzing its average and worst-case time complexities. It then explains the order selection problem, which involves finding the kth smallest element in a dataset, presenting several algorithms with varying time complexities and practical consi…

1
Recurrence Equations and Asymptotic Notation 19:30

11M ago19:30

19:30

This episodes presents methods for solving recurrence equations, which are crucial for analyzing the time complexity of recursive algorithms. It introduces asymptotic notations (Big O, Big Omega, Big Theta, little o, little omega) to describe the growth of functions. The lecture then explores several techniques for solving recurrences, including th…

1
Physics and Computer Science 12:31

11M ago12:31

12:31

The 2024 Nobel Prize in Physics was awarded to John Hopfield and Geoffrey Hinton for their foundational work on artificial neural networks (ANNs). The award citation highlights their contributions to machine learning, linking ANNs to concepts in physics, such as spin models and statistical mechanics. Hopfield's research focused on recurrent network…

1
Combinatorics: Counting and Permutations 20:42

11M ago20:42

20:42

This episode focuses on fundamental counting principles. It covers the product rule, sum rule, and subtraction rule for counting the number of ways to perform tasks that can be broken down into subtasks. Additionally, it explores the pigeonhole principle, counting in two different ways, and the relationship between permutations and combinations.…

1
Introduction to Formalizing Programming Languages Theory 12:20

11M 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
Unlocking the Secrets of Sentential Logic 13:38

11M ago13:38

13:38

Dive into the fascinating world of sentential logic! In this episode, we explore the foundations of propositional logic, the art of constructing truth tables, and how logical connectives like "and," "or," and "not" shape our reasoning. Whether you're a philosophy enthusiast, a math lover, or just curious about how we break down complex arguments in…

1
Introduction to Graph Theory 19:44

11M ago19:44

19:44

This episode explores key concepts in graph theory, starting with fundamental definitions of graphs, vertices, and edges. The text then examines the handshake lemma and related theorems that deal with the relationship between vertex degrees and the number of edges in a graph.By AmCan Tech

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

1+ y 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

1+ y 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
The curious case of exponentiation in simply typed lambda calculus 7:29

1+ y 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
Arithmetic operations in simply typed lambda calculus 9:56

1+ y 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
More on basics of simple types 15:45

1+ y 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

2+ y 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

2+ y 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

2+ y 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

2+ y 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

2+ y 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

2+ y 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…