Formalizing proofs in Isabelle/HOL of equational properties for the lambda-calculus using one-sorted variable names. Honours dissertation, University of Edinburgh; available from the author’s homepage, 2001. 29 Rod Burstall. Proving properties of programs

Abstract: We present the Isabelle/HOL formalisation of some key equa-tional properties of the untyped λ-calculus with one-sorted variable names. Existing machine formalisations of λ-calculus proofs typically rely on alterna-tive representations and/or proof principles to facilitate mechanization and we briefly account for these works. Our own development remains faithful to the standard textbook presentation and the usual pen-and-paper proof practices; we reason purely inductively over the standard first-order syntax of the calculus, using only primitive proof principles of the syntax and the reduction relations under consideration. We prove the confluence property of the λ-calculus at the raw syntactic level and derive confluence of the real λ-calculus (the structural collapse onto equivalence classes of the raw calculus) via a general result about abstract rewrite systems which we also formalise. We then show a technical property of the residual theory of the calculus which suggests the general appli-cability of the method to other equational properties of the calculus. Finally, we make some proof-technical observations pertaining to the extent to whic