 @article{MilnerPoly,author="Robin Milner", title="A Theory of Type Polymorphism in Programming", journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348375"}  
which also proves their correctness. The first completeness proof was given in 
 @phdthesis{DamasPhD,author={Luis Manuel Martins Damas}, title={Type Assignment in Programming Languages}, school={Department of Computer Science, University of Edinburgh},year=1985}  
The Isabelle proofs are based on 
 @phdthesis{NazarethPhD,author={Dieter Nazareth}, title={A Polymorphic Sort System for Axiomatic Specification Languages}, school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen}, year=1995,note={Technical Report {TUMI9515}}}  +This theory defines the type inference rules and the type inference algorithm +W for simplytyped lambda terms due to Milner. It proves the +soundness and completeness of W w.r.t. to the rules. An optimized +version I is shown equivalent to W (one direction only). +
