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.

Robert Recorde Room

Department of Computer Science