Mechanising lambda-calculus using a classical first order theory of terms with permutations

Michael Norrish. Mechanising lambda-calculus using a classical first order theory of terms with permutations. Higher-Order and Symbolic Computation, 19(2-3):169-195, 2006. [doi]

Abstract

Abstract is missing.