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 .