Iowa Type Theory Commute
163 episodes - English - Latest episode: 7 months ago - ★★★★★ - 13 ratingsAaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Homepage Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Episodes
Some advanced examples in DCS
September 25, 2023 03:00 - 23 minutes - 16 MBThis 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 ensures that they are terminating on all inputs.
DCS compared to termination checkers for type theories
September 19, 2023 03:00 - 19 minutes - 13.6 MBIn 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.
Getting started with DCS
September 10, 2023 04:00 - 17 minutes - 12 MBIn 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
September 04, 2023 04:00 - 11 minutes - 8 MBDCS 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.
Semantics of subtyping
July 24, 2023 03:00 - 15 minutes - 10.6 MBI 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 <: B by c", where c is a function from A to B. The idea is that the compiler should automatically insert calls to c whenever an expression of type A needs to be ...
More on type inference for simple subtypes
July 16, 2023 02:00 - 9 minutes - 6.28 MBI continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.
Subtyping, the golden key
July 09, 2023 03:00 - 9 minutes - 6.37 MBIn 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 for applicative functors/monads.
Type inference with simple subtypes
June 30, 2023 04:00 - 13 minutes - 9.27 MBIn 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 telegram group for discussion related to the podcast.
Basics of subtyping
June 21, 2023 21:00 - 8 minutes - 5.59 MBIn 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.
Begin chapter on subtyping
June 21, 2023 03:00 - 16 minutes - 11.2 MBWe 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 for practical strong functional programming, where the language has a pure, terminating core language, then a monad for pure but possibly diverg...
Last episode discussing Observational Equality Now for Good
April 13, 2023 05:00 - 12 minutes - 8.45 MBIn 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 the new Telegram group for the podcast if you want to discuss episodes.
More on observational type theory
March 23, 2023 05:00 - 13 minutes - 9.45 MBI 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 news, I created a Telegram group that you can join if you want to discuss topics related to the podcast or particularly podcast episodes. I wil...
Introduction to Observational Type Theory
March 06, 2023 05:00 - 10 minutes - 7.02 MBIn 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 statements of extensional equality for the type of the values being equated.
Interjection: The Liquid Tensor Experiment
March 02, 2023 06:00 - 12 minutes - 8.55 MBI 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, when a theorem was formalized in a theorem prover, in order to resolve doubts of the mathematician who proved it. An amazing achievement. This ep...
Extensional Martin-Loef Type Theory
February 04, 2023 05:00 - 11 minutes - 7.86 MBIn 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 definitionally equal. This immediately gives us undecidability of type checking for the theory, at least as usually realized.
Begin chapter on extensionality
January 25, 2023 05:00 - 10 minutes - 7.21 MBThis 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 mergesort are equal, even though their codes are not syntactically equivalent. The episode begins by reviewing the distinction between definitional an...
Papers from Formal Methods for Blockchains 2021
January 01, 2023 20:00 - 17 minutes - 11.7 MBIn 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 then search for Computer Science. Select the Computer Science Development Fund, College of Liberal Arts and Sciences. Then add gift instructions ...
Mi-Cho-Coq: Michelson formalized and applied, in Coq
December 02, 2022 06:00 - 15 minutes - 10.7 MBIn 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 ($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 ...
Verification of Tezos smart contracts with K-Michelson
November 11, 2022 05:00 - 14 minutes - 9.93 MBIn 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.
Verification of Tezos smart contracts with K-Michelson
November 11, 2022 05:00 - 14 minutes - 9.93 MBIn 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.
Start of Season 3: Formal Methods for Blockchain
November 07, 2022 06:00 - 10 minutes - 7.57 MBI 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.
Start of Season 4: Formal Methods for Blockchain
November 07, 2022 06:00 - 10 minutes - 7.57 MBI 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.
Separation Logic II: recursive predicates
September 16, 2022 04:00 - 11 minutes - 8.18 MBI 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.
Separation Logic 1
July 25, 2022 03:00 - 13 minutes - 9.26 MBI 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.
Let's talk about Rust
July 10, 2022 03:00 - 13 minutes - 9.5 MBIn 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.
Region-Based Memory Management
June 22, 2022 03:00 - 16 minutes - 11.7 MBI 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 entire region may be deallocated. Type inference is used to make sure that no dangling pointers are dereferenced (after the associated region is d...
Introduction to verified memory management
June 05, 2022 04:00 - 17 minutes - 11.8 MBIn 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 memory-usage properties of programs is challenging in proof assistants.
More on Metamath
May 21, 2022 03:00 - 17 minutes - 11.9 MBI 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.
Metamath
April 23, 2022 21:00 - 14 minutes - 10 MBIn 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 easy to download and try out.
The Seventeen Provers of the World
April 10, 2022 04:00 - 10 minutes - 7.31 MBI 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 Lean, which was created after that year. Happily, you can find a PDF of the book here, on Wiedijk's web site.
More on Lean
March 13, 2022 04:00 - 15 minutes - 10.5 MBI talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.
The Lean Prover
February 28, 2022 04:00 - 14 minutes - 10.2 MBIn 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.
More on Isabelle, and the Complexity of ITPs
February 17, 2022 04:00 - 16 minutes - 11.2 MBI talk about my attempts to use Isabelle as a newbie, and reflect a little on the complexity of both Isabelle and Coq.
Isabelle/HOL
January 28, 2022 05:00 - 16 minutes - 11.6 MBThe 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.
More on Agda
January 13, 2022 01:00 - 13 minutes - 9 MBI talk a bit more about the Agda proof assistant.
A look at Agda
January 10, 2022 05:00 - 15 minutes - 10.6 MBIn this episode I talk a bit about the Agda proof assistant.
More reflections on Coq
December 31, 2021 23:00 - 18 minutes - 12.7 MBI 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.
The Coq Proof Assistant
December 29, 2021 04:00 - 15 minutes - 10.4 MBI discuss Coq, a widely used proof assistant based on a constructive type theory. One episode definitely cannot do justice to the complexity of a tool like this -- but I take a first try at covering its features at a high level.
Introduction to Interactive Theorem Provers
December 17, 2021 04:00 - 11 minutes - 8.25 MBThis is the start of Chapter 15, about interactive theorem provers (ITPs). In this episode, I talk about the difference between fully automatic and interactive provers, and my plan to discuss and compare several different ITPs, in future episodes of this chapter.
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
December 11, 2021 04:00 - 14 minutes - 9.77 MBIn 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 explanation has something of a hole, in explaining how one would go about deriving induction for ordinals strictly less than epsilon-0 in Peano Arithmetic. To help paper over this hole a little, I discuss a really nice recent exposition of encoding ordinals in Agda.
The proof-theoretic ordinal of a logical theory
November 21, 2021 05:00 - 12 minutes - 8.43 MBOrdinal analysis seeks to determine the strength of a logical theory by assigning an ordinal to it. Which one? In this episode I describe a definition of the proof-theoretic ordinal of a logical theory from a paper by proof theorist Michael Rathjen. It is basically a measure of how strong an induction principle is derivable in the theory. (The first parts of the paper are pretty accessible, but the rest gets hard, at least for me.)
Introduction to Ordinal Analysis
November 17, 2021 03:00 - 14 minutes - 10.1 MBOrdinal analysis is an important branch of proof theory, which seeks to compare, quantitatively, the strengths of different proof systems. The quantities in question are ordinals, which extend the ordering character of natural numbers into the infinite. In this episode, I discuss these ideas a bit further, and also review a little the ordinals up to epsilon 0.
An analogy for multiplicative disjunction
November 03, 2021 05:00 - 11 minutes - 7.87 MBListen 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 and intuitive example of multiplicative disjunction.
Linear conjunctions and disjunctions
October 29, 2021 03:00 - 12 minutes - 8.28 MBI explain the basic idea of multiplicative versus additive proof rules, and consider multiplicative conjunction (tensor), addition conjunction (&, "with"), additive disjunction -- but leaving multiplicative disjunction (par) for next time!
A taste of linear logic
October 22, 2021 04:00 - 11 minutes - 8.1 MBWe 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
October 13, 2021 04:00 - 12 minutes - 8.9 MBIn 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
October 05, 2021 05:00 - 12 minutes - 8.34 MBCut elimination for sequent calculus is more involved that normalization of detours for natural deduction. There are more cases of cuts that must be transformed than correspond to detours (introductions followed by eliminations). In this episode, I explain why that is.
Introduction to Cut Elimination
September 29, 2021 05:00 - 9 minutes - 6.25 MBWe saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is immediately followed by an elimination inference on the introduced formula. What corresponds to this for sequent calculus proofs? The answer is cut elimination. This episode describes the cut rule and what is meant by a cut-elimination procedure. We will talk more about such a procedure in the next episode.
Normalization of detours for implication inferences
September 19, 2021 21:00 - 12 minutes - 8.82 MBWe talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implication rules. Under Curry-Howard, this actually corresponds to beta-reduction, and could make the proof bigger (though less complex in a certain sense).
Normalization in natural deduction
September 18, 2021 05:00 - 10 minutes - 7.41 MBThis episode explains the idea of normalization of proofs in natural deduction. We want to eliminate so-called detours in proofs, which occur when an introduction is immediately followed by an elimination.