Higher-Order and Symbolic Computation, 19(2/3)
Mechanising lambda-calculus using a Classical First Order Theory of Terms with Permutations
Michael Norrish, Canberra Research Laboratory, National ICT Australia, Australian National University, Acton, Australia
|
Abstract: This paper describes the mechanisation in HOL of some basic lambda-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. |
This article is not yet available.
![[picture of journal cover]](../LISP.JPG)