Krivine's Proof of FD, Using Intersection Types
05 May 2025

Krivine's Proof of FD, Using Intersection Types

Iowa Type Theory Commute

About

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.