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


Related publications

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

Session MiniML