Mini ML

Wolfgang Naraschewski and Tobias Nipkow 🌐

March 19, 2004


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.
BSD License


Theories of MiniML