[an error occurred while processing this directive]
An error occured whilst processing this directive
Inductions in the Nominal Datatype Package (or, How Not to be
Intimidated by the Variable Convention)
TU Munich
4pm Tuesday 29th May 2007
Room 2511, JCMB, King's Buildings
Abstract
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.
An error occured whilst processing this directive