#### Formal Verification of Algorithm W: The Monomorphic Case

#### Dieter Nazareth and Tobias Nipkow

A formal verification of the soundness and completeness of Milner's type
inference algorithm W for simply typed lambda-terms is presented. Particular
attention is paid to the notorious issue of ``new'' variables. The proofs are
carried out in Isabelle/HOL, the HOL instantiation of the generic theorem
prover Isabelle.
dvi

BibTeX:

@inproceedings{Nazareth-Nipkow,
author={Dieter Nazareth and Tobias Nipkow},
title={Formal Verification of Algorithm {W}: The Monomorphic Case},
booktitle={Theorem Proving in Higher Order Logics (TPHOLs'96)},
editor={J. von Wright and J. Grundy and J. Harrison},
publisher=Springer,series=LNCS,volume=1125,pages={331--346},
url={http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.dvi.gz},
year=1996}

This work has been extended by Naraschewski and Nipkow
to include `let``.
`