#### Type Inference Verified: Algorithm W in Isabelle/HOL

This paper presents the first machine-checked verification of Milner's
type inference algorithm W for computing the most general
type of an untyped lambda-term enriched with
`let`-expressions. This term language is the core of most typed
functional programming languages and is also known as Mini-ML. We
show how to model all the concepts involved, in particular types and
type schemes, substitutions, and the thorny issue of ``new''
variables. Only a few key proofs are discussed in detail. The theories
and proofs are developed in Isabelle/HOL, the HOL instantiation of the
generic theorem prover Isabelle.
Short version: ps

BibTeX:

@inproceedings{Naraschewski-Nipkow-TYPES96,
author={Wolfgang Naraschewski and Tobias Nipkow},
title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
booktitle={Types for Proofs and Programs: Intl. Workshop TYPES '96},
editor={E. Gim\'enez and C. Paulin-Mohring},
publisher=Springer,series=LNCS,volume=1512,pages={317--332},year=1998}

Long version: dvi

BibTeX:

@article{NaraschewskiN-JAR,
author={Wolfgang Naraschewski and Tobias Nipkow},
title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
journal={Journal of Automated Reasoning},
year=1999,volume=23,pages={299--318}}

The corresponding
Isabelle theories.
This work is based on the earlier work of
Nazareth and Nipkow
which did not include `let``.
`