Personal tools
You are here: Home Events Abstract Archives 2006-2007 Inductions in the Nominal Datatype Package (or, How Not to be Intimidated by the Variable Convention)

Inductions in the Nominal Datatype Package (or, How Not to be Intimidated by the Variable Convention)

Christian Urban TU Munich 4pm Tuesday 29th May 2007 Room 2511, JCMB, King's Buildings

In informal proofs about the lambda-calculus (and other calculi with binders), one often assumes a variable convention in order to obtain simple proofs. Unfortunately, this convention is usually not formally justified, which makes it hard to formalise such proofs. In this talk I will first give an overview about the nominal datatype package we are implementing on top of Isabelle/HOL; and then will give more details about strong induction principles that have the variable convention already built in. How one can derive them and how they are used will be explained next. I conclude with an overview about formalisation we and others have already done using those strong induction principles.

Document Actions