Iowa Type Theory Commute

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

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

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 ensures that they are terminating on all in...

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 . 

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

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.  

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 <: B by c", where c is a function from A to B. ...

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

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 for applicative functors/monads.

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 telegram group for discussion related to...

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.

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 for practical strong functional programming, whe...

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 the new Telegram group for the...

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 news, I created a Telegram group that...

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 statements of extensional equality for the typ...

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, when a theorem was formalized in a theorem prover,...

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 definitionally equal.  This immediately gives us undecidabil...

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 mergesort are equal, even though their codes are not sy...

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 then search for Computer Scie...

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 ($5 or $10 would be awesome) to pay my...

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.

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.

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.

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.

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.