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.

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: