Iowa Type Theory Commute

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

  --------  

  7:10
• 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.

  --------  

  21:35
• 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.

  --------  

  23:24
• 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 their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate.  In this episode, I discuss the theorem and why I got interested in it.

  --------  

  15:54
• 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 modulo alpha-equivalence, using ideas from nominal logic.  The basic idea is that instead of renamings, one works with permutations of names. 

  --------  

  16:18

Plus de podcasts Technologies

Podcasts tendance de Technologies

À propos de Iowa Type Theory Commute