Mini ML

Wolfgang Naraschewski and Tobias Nipkow 🌐

March 19, 2004

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.

License

BSD License

Topics

Related publications

  • Naraschewski, W., & Nipkow, T. (1999). Journal of Automated Reasoning, 23(3), 299–318. https://doi.org/10.1023/a:1006277616879
  • author's copy

Session MiniML

Cite

× 
@article{MiniML-AFP,
  author  = {Wolfgang Naraschewski and Tobias Nipkow},
  title   = {Mini ML},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2004},
  note    = {\url{https://isa-afp.org/entries/MiniML.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: