About
I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church. One reason to do that, besides just a love of being ornery, is to be able to state and prove theorems about alpha-equivalence. One example class of such theorems concern when alpha-equivalence can be avoided, in the sense that beta-reduction can proceed without any variable capture, while not requiring renaming variables. I have a companion blog post that talks about this, with a link to the repo with my Agda code so far.