A Fireball of Alpha
I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church....
Radio and PodcastLive Radio & PodcastsTechnology
Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Episodes
20 of 190 episodesSolving Quadratic Word Equations
A system of word equations is called quadratic if no variable occurs more than twice in it. There is an interesting simple algorithm to solv...
A little bit about word equations
The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tenth problem. Word equations relate ex...
Coercive subtyping and coherence
In this episode, I give further arguments in favor of coercive subtyping from a software-engineering perspective. I also explain the critica...
A Strange Deal, Explained
I explain the story from last episode.
A Strange Deal
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...
Great paper: The Calculated Typer
I discuss a nice paper I quite enjoyed reading, called The Calculated Typer , by Garby, Bahr, and Hutton. The authors take a very nice gener...
Double-negation translations and CPS conversion, part 2
In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CP...
Double-negation translations and CPS conversion, part 1
In this episode, I talk about a somewhat more advanced case of the Curry-Howard isomorphism (the connection between logic and programming la...
What are commuting conversions in proof theory?
Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the nor...
What is Control Flow Analysis for Lambda Calculus?
I am currently on a frolic into the literature on Control Flow Analysis (CFA), and discuss what this is, for pure lambda calculus. A wonderf...
Measure Functions and Termination of STLC
In this episode, I talk about what we should consider to be a measure function. Such functions can be used to show termination of some proce...
Schematic Affine Recursion, Oh My!
To solve the problem raised in the last episode, I propose schematic affine recursion. We saw that affine lambda calculus (where lambda-boun...
The Stunner: Linear System T is Diverging!
In this episode, I shoot down last episode's proposal -- at least in the version I discussed -- based on an amazing observation from an...
Terminating Computation First?
In this episode, I discuss an intriguing idea proposed by Victor Taelin, to base a logically sound type theory on an untyped but terminating...
Correction: the Correct Author of the Proof from Last Episode, and an AI flop
I correct what I said in the last episode about the author of the proof of FD from last episode based on intersection types. I also describe...
Krivine's Proof of FD, Using Intersection Types
Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types. I discuss this proof in this...
A Measure-Based Proof of Finite Developments
I discuss the paper "A Direct Proof of the Finite Developments Theorem" , by Roel de Vrijer. See also the write-up at my blog.
Introduction to the Finite Developments Theorem
The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and...
Nominal Isabelle/HOL
In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL , by Christian Urban. This paper shows how to reason with terms modu...