[L4] ================================================ AMAST Links 03 01

       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.

  The paper documents HOL's subtheory MiniML and is available via URL:
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W0.html