Latest Computational logic Podcast Episodes
Turing's proof of normalization for STLC
Iowa Type Theory Commute - May 21, 2024 03:00 - 17 minutes ★★★★★ - 13 ratingsIn 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.
Introduction to normalization for STLC
Iowa Type Theory Commute - May 14, 2024 04:00 - 9 minutes ★★★★★ - 13 ratingsIn 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 anythin...
Arithmetic operations in simply typed lambda calculus
Iowa Type Theory Commute - May 04, 2024 14:00 - 9 minutes ★★★★★ - 13 ratingsIt 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 ...
The curious case of exponentiation in simply typed lambda calculus
Iowa Type Theory Commute - May 04, 2024 14:00 - 7 minutes ★★★★★ - 13 ratingsLike 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 as...
More on basics of simple types
Iowa Type Theory Commute - April 29, 2024 15:00 - 15 minutes ★★★★★ - 13 ratingsI review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
Begin Chapter on Simple Type Theory
Iowa Type Theory Commute - April 19, 2024 16:00 - 15 minutes ★★★★★ - 13 ratingsIn 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...
Some advanced examples in DCS
Iowa Type Theory Commute - September 25, 2023 03:00 - 23 minutes ★★★★★ - 13 ratingsThis 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 t...
DCS compared to termination checkers for type theories
Iowa Type Theory Commute - September 19, 2023 03:00 - 19 minutes ★★★★★ - 13 ratingsIn 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
Iowa Type Theory Commute - September 10, 2023 04:00 - 17 minutes ★★★★★ - 13 ratingsIn 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
Iowa Type Theory Commute - September 04, 2023 04:00 - 11 minutes ★★★★★ - 13 ratingsDCS 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
Iowa Type Theory Commute - July 24, 2023 03:00 - 15 minutes ★★★★★ - 13 ratingsI 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 s...
More on type inference for simple subtypes
Iowa Type Theory Commute - July 16, 2023 02:00 - 9 minutes ★★★★★ - 13 ratingsI continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.
Subtyping, the golden key
Iowa Type Theory Commute - July 09, 2023 03:00 - 9 minutes ★★★★★ - 13 ratingsIn 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 mon...
Type inference with simple subtypes
Iowa Type Theory Commute - June 30, 2023 04:00 - 13 minutes ★★★★★ - 13 ratingsIn 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...
Basics of subtyping
Iowa Type Theory Commute - June 21, 2023 21:00 - 8 minutes ★★★★★ - 13 ratingsIn 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
Iowa Type Theory Commute - June 21, 2023 03:00 - 16 minutes ★★★★★ - 13 ratingsWe 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 t...
Last episode discussing Observational Equality Now for Good
Iowa Type Theory Commute - April 13, 2023 05:00 - 12 minutes ★★★★★ - 13 ratingsIn 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 Dyb...
More on observational type theory
Iowa Type Theory Commute - March 23, 2023 05:00 - 13 minutes ★★★★★ - 13 ratingsI 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 ...
Introduction to Observational Type Theory
Iowa Type Theory Commute - March 06, 2023 05:00 - 10 minutes ★★★★★ - 13 ratingsIn 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 ha...
Interjection: The Liquid Tensor Experiment
Iowa Type Theory Commute - March 02, 2023 06:00 - 12 minutes ★★★★★ - 13 ratingsI 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....
Extensional Martin-Loef Type Theory
Iowa Type Theory Commute - February 04, 2023 05:00 - 11 minutes ★★★★★ - 13 ratingsIn 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 t...
Begin chapter on extensionality
Iowa Type Theory Commute - January 25, 2023 05:00 - 10 minutes ★★★★★ - 13 ratingsThis 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...
Papers from Formal Methods for Blockchains 2021
Iowa Type Theory Commute - January 01, 2023 20:00 - 17 minutes ★★★★★ - 13 ratingsIn 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...
Mi-Cho-Coq: Michelson formalized and applied, in Coq
Iowa Type Theory Commute - December 02, 2022 06:00 - 15 minutes ★★★★★ - 13 ratingsIn 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 Multisi...
Verification of Tezos smart contracts with K-Michelson
Iowa Type Theory Commute - November 11, 2022 05:00 - 14 minutes ★★★★★ - 13 ratingsIn 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 contrac...
Verification of Tezos smart contracts with K-Michelson
Iowa Type Theory Commute - November 11, 2022 05:00 - 14 minutes ★★★★★ - 13 ratingsIn 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 contrac...
Start of Season 4: Formal Methods for Blockchain
Iowa Type Theory Commute - November 07, 2022 06:00 - 10 minutes ★★★★★ - 13 ratingsI 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 3: Formal Methods for Blockchain
Iowa Type Theory Commute - November 07, 2022 06:00 - 10 minutes ★★★★★ - 13 ratingsI 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
Iowa Type Theory Commute - September 16, 2022 04:00 - 11 minutes ★★★★★ - 13 ratingsI 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
Iowa Type Theory Commute - July 25, 2022 03:00 - 13 minutes ★★★★★ - 13 ratingsI 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.
Related Computational logic Topics