Christian Urban, Michael Norrish. A formal treatment of the barendregt variable convention in rule inductions. In Randy Pollack, editor, ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005. pages 25-32, ACM, 2005. [doi]
Abstract is missing.