Iowa Type Theory Commute · May 5, 2025 · 21 min

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 episode.

0:00-21:35

transcript

No transcript — this publisher did not publish one.

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.

links1