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.


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


Related publications

  • Naraschewski, W., & Nipkow, T. (1999). Journal of Automated Reasoning, 23(3), 299–318.
  • author's copy

Session MiniML