Nominal Techniques in the Theorem Prover Isabelle or, How Not to be Intimidated by the Variable Convention

Photograph of Christian Urban

Christian Urban

(TU München)

Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal proofs,
especially in proofs by induction. In informal proofs by induction
one often assumes a variable convention in order to sidestep all
problems and 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 show how strong induction principles
can be formally derived that have the variable convention already
built in. I will also show that the variable convention depends on
some non-trivial conditions in order to be a sound reasoning principle.
The aim of this work is to provide all proving technology necessary
for reasoning conveniently about the lambda-calculus and programming
languages.

Tuesday 1st April 2008, 14:00
Robert Recorde Room
Department of Computer Science