René Vestergaard, James Brotherston. A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings. Volume 2051 of Lecture Notes in Computer Science, pages 306-321, Springer, 2001. [doi]
Abstract is missing.