Abstract:
No matter how much one probes the specification of a programming language for errors, to ensure that a programming language is correct one needs to give a mathematical proof. For small idealised programming languages proofs with "pencil and paper" are enough, but for non-trivial languages one needs to have computer support and correctness proofs that can be checked by machine.
In this talk a technique will be described for implementing with ease machine checkable proofs about the lambda-calculus. This work is based on the nominal approach to binders where terms have names in abstractions. A nominal datatype package, currently under development in the theorem prover Isabelle/HOL, is designed to help establishing the correctness of programming languages. The talk will describe some of the mathematical ideas behind this datatype package.