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

Norrish, Michael2015-12-081388-3690http://hdl.handle.net/1885/31081This paper describes the mechanisation in HOL of some basic λ-calculus theory. The proofs are taken from standard sources (books by Hankin and Barendregt), and cover: equational theory, reduction theory, residuals, finiteness of developments, and the staKeywords: Combinatorial mathematics; Computational complexity; Numerical methods; Theorem proving; ?-calculus theory; HOL; Standardisation theorem; Differentiation (calculus)Mechanising lambda-calculus using a classical first order theory of terms with permutations200610.1007/s10990-006-8745-72015-12-08