Episodes
188
Latest episode
Aug 2026
Language
EN-US
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
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 .
In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming languages where formulas in logic are identified with types, and proofs with programs). This is the identification of double-negation translations in logic, which go back to a paper of Kolmogorov's in 1925, with conversion to continuation-passing style (CPS), a compilation technique. For this episode, we just discuss the idea of double-negation translation: classical theorems can be translated to intuitionistic ones, by adding some double negations. As an example, we talk through the intuitionistic proof of the double negation of the law of excluded middle: not not (p or not p).
Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled. The stuck inferences are uses of disjunction elimination. In programming terms, if you have an if-then-else (a simple case of or-elimination) where the then- and else-branches are lambda abstractions, and you apply that if-then-else to an argument, you need commuting conversions to move the argument into the branches, so you can call the functions (in the then- and else-branches) with it. See Section 10.1 of Girard's Proofs and Types for more on the problem, and a nice paper by de Groote on strong normalization with commuting conversions.
I am currently on a frolic into the literature on Control Flow Analysis (CFA), and discuss what this is, for pure lambda calculus. A wonderful reference for this is this paper by Palsberg.
Claim this listing to keep it up to date, reach guests who want to pitch you, and manage bookings with Guestify.
Claim this listingMSP Radio
Earth Notes / Damon Hart-Davis
Anthony Fasano, PE, AEC PM, F. ASCE and James Taylor, JR., P.E.
Anthony Fasano, PE & Nick Heim, PE
