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 termination already for the untyped language, we no longer have to make the type system do the heavy work of enforcing termination.

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 [email protected], or join the Telegram group for the podcast.  

I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem.  The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.

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.