Iowa Type Theory Commute

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 write-up at my blog.

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.

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. 

I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud.  I complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction.  I also answer a listener's question about what "computational type theory" means.  Feel free to email me any time at aaron.stump@bc.edu, or join the Telegram group for the podcast.  

I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations, which proposes a benchmark problem for mechanizing Programming Language theory.  

In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers like Rocq (formerly Coq) and Agda.

In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s.  See this short note for Turing's original proof and some historical comments.

In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods.  We will look at proofs in more detail in the coming episodes.  Feel free to join the Telegram group for the podcast if you want to discuss anything (or just email me at aaron.stump@gmail.com).