Department of Mathematics
Ludwig-Maximilians-Universitat
Munich
4pm, Tuesday 25 January 2005
Room 2511, JCMB, King's Buildings
I will describe how standard (informal) proofs about the lambda-calculus can be formalised in Isabelle/HOL using a variant of Pitts' nominal logic approach to binders. First, I present an inductive definition for alpha-equated lambda-terms and then a strong induction principle, which looks very much like the Barendregt variable convention.