TY - JOUR
T1 - Mechanising λ-calculus using a classical first order theory of terms with permutations
AU - Norrish, Michael
PY - 2006/9
Y1 - 2006/9
N2 - 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 standardisation theorem. The issues in mechanising pen-and-paper proofs are discussed; in particular, those difficulties arising from the sources' use of the Barendregt Variable Convention.
AB - 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 standardisation theorem. The issues in mechanising pen-and-paper proofs are discussed; in particular, those difficulties arising from the sources' use of the Barendregt Variable Convention.
UR - http://www.scopus.com/inward/record.url?scp=33747268056&partnerID=8YFLogxK
U2 - 10.1007/s10990-006-8745-7
DO - 10.1007/s10990-006-8745-7
M3 - Article
SN - 1388-3690
VL - 19
SP - 169
EP - 195
JO - Higher-Order and Symbolic Computation
JF - Higher-Order and Symbolic Computation
IS - 2-3
ER -