Nominal verification of algorithm W

Christian Urban Tobias Nipkow

The Milner-Damas typing algorithm W is one of the classic algorithms in Computer Science. In this paper we describe a formalised soundness and completeness proof for this algorithm. Our formalisation is based on names for both term and type variables, and is carried out in Isabelle/HOL using the Nominal Datatype Package. It turns out that in our formalisation we have to deal with a number of issues that are often overlooked in informal presentations of W.



author={Christian Urban and Tobias Nipkow},
title={Nominal verification of algorithm {W}},
booktitle={From Semantics to Computer Science. Essays in Honour of Gilles Kahn},
editor={G. Huet and J.-J. Lévy and G. Plotkin},
publisher={Cambridge University Press},pages={363--382},year=2009}