A Fireball of Alpha

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.