Mechanising Hankin and Barendregt using the Gordon-Melham axioms
Michael Norrish · 2003
I describe the mechanisation in HOL of some basic λ-calculus theory, using the axioms proposed by Gordon and Melham [4]. Using these as a foundation, I mechanised the proofs from Chapters 2 and 3 of Hankin [5] (equational theory and reduction theory), followed by most of Chapter 11 of Barendregt [2] (residuals, finiteness of developments, and the standardisation theorem). I discuss the ease of use of the Gordon-Melham axioms, as well as the mechanical support I implemented to make some basic tasks more straightforward.