Mechanising Hankin and Barendregt using the Gordon-Melham axioms

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. Categories and Subject Descriptors F.4.1 [Mathematical Logic]: Lambda calculus and related systems; I.2.3 [Deduction and Theorem Proving]: Deduction General Terms Theory, Verification Keywords ive theorem-proving, higher order abstract syntax

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Michael Norrish
• Keywords: Basic -calculus Theory, Equational Theory, General Terms Theory, ICFP 2003, Programming Languages