Verification by Formalisation, Or How Not to be Intimidated by the Variable Convention

Christian Urban, TU Muenchen

 

In 2005 in a journal paper, Harper and Pfenning proved a result in programming language research (the correctness of an equality- checking algorithm). We formalised this result and during the formalisation had to fix a gap. We found three fixes for the problem.  In the first part of the talk I will describe which lessons we learned from this formalisation, which go beyond the fact that formalisations are important for ensuring validity of results in programming language research.

 

In the second part, I will describe the techniques we introduced in order to be able to formalise the result of Harper and Pfenning.

I will show how induction principles need to be strengthened so that they have the commonly used convention about  bound variables already built-in. However, I will also show that this convention is in general an unsound reasoning principle and requires restrictions in order to be safe. The aim of this work is to provide all proving technology necessary for reasoning conveniently about programming languages, programs and logic calculi.