# Nominal Reasoning Techniques in Isabelle/HOL

Christian Urban 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.