In this episode, I discuss an intriguing idea proposed by Victor Taelin, to base a logically sound type theory on an untyped but terminating language, upon which one may then erect as exotic a type system as one wishes.  By enforcing termi...

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 AI flopping when I ask it a question about this.

Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types.  I discuss this proof in this episode.

I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer.  See also the

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 their residuals (redexes that can be traced back as existing in the original set), then this process wi...