This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.
This theory defines the type inference rules and the type inference algorithm W for MiniML (simply-typed lambda terms with let) due to Milner. It proves the soundness and completeness of W w.r.t. the rules.