Coercive subtyping and coherence

I start discussing this great paper by Dunfield and Krishnaswami, about how to extend a particular approach to type inference to handle polymorphism.

In this episode, I reflect on the recent announcement that Anthropic researchers have autoformalized the proof of Fermat's Last Theorem.  That is, they instructed an LLM to create a computer-checkable proof, in the Lean prover, of this theorem, following existing paper proofs in the literature.  The resulting proof weighs in at 13 million lines of Lean, a staggering amount.

I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church.  One reason to do that, besides just a love of being ornery, is to be able to state and prove theorems about alpha-equivalence.  One example class of such theorems concern when alpha-equivalence can be avoided, in the sense that beta-reduction can proceed without any variable capture, while not requiring renaming variables.  I have a companion blog post that talks about this, with a link to the repo with my Agda code so far.

A system of word equations is called quadratic if no variable occurs more than twice in it.  There is an interesting simple algorithm to solve quadratic systems of word equations, which I talk through in this episode.  My source is Chapter 12 of "Algebraic Combinatorics on Words" by Lothaire.

The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tenth problem.  Word equations relate expressions consisting of concatenations of variables and constant symbols.  An example is a X = X a, where X is a variable and a is a constant.  A solution maps variables to strings of constant symbols making the two sides identical.  In this episode, I discuss the problem a little, and what I learned so far about how it is solved.

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering perspective.  I also explain the critical concept of coherence.

I explain the story from last episode.

The Curry-Howard isomorphism for the law of excluded middle, as a radio drama.  I first saw a version of this story performed by Phil Wadler and Frank Pfenning (wearing fake horns!) at RTA in Nara, Japan in 2005.  This is my take on it.  In a subsequent episode, I will explain how the story illustrates the computational interpretation of the law of excluded middle.

I discuss a nice paper I quite enjoyed reading, called The Calculated Typer, by Garby, Bahr, and Hutton.  The authors take a very nice general look at the specification of a type checker, for a very simple expression language.  They then manually derive the actual code for the type checker by effectively trying to prove that this as yet unknown code satisfies its spec.  (This is what is meant by calculating the type checker.)

In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CPS).  I sketch how CPS conversion (transforming a program with callcc into one in CPS that does not need callcc any more) corresponds to double-negation translation from classical to intuitionistic logic.  The paper I am referencing is here.