Mini ML

Wolfgang Naraschewski and Tobias Nipkow 🌐

March 19, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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

Topics

Theories of MiniML