Mechanising lambda-calculus using a classical first order theory of terms with permutations
This 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 sta
|Collections||ANU Research Publications|
|Source:||Higher-Order and Symbolic Computation|
|01_Norrish_Mechanising_lambda-calculus_2006.pdf||293.3 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.