ML is a general-purpose functional programming language developed by Robin Milner and others in the late 1970s at the University of Edinburgh,[1] whose syntax is inspired by ISWIM. Historically, ML stands for metalanguage: it was conceived to develop proof tactics in the LCF theorem prover (whose language, pplambda, a combination of the first-order predicate calculus and the simply typed polymorphic lambda-calculus, had ML as its metalanguage). It is known for its use of the Hindley-Milner type inference algorithm, which can automatically infer the types of most expressions without requiring explicit type annotations.