- Info

#
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.