I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer.  See also the

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

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

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

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