ML is a general-purpose functional programming language developed by Robin Milner

Robin Milner

Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...

 and others in the early 1970s at the University of Edinburgh

University of Edinburgh

The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...

, whose syntax is inspired by ISWIM

ISWIM

ISWIM is an abstract computer programming language devised by Peter J. Landin and first described in his article, The Next 700 Programming Languages, published in the Communications of the ACM in 1966...

. Historically, ML stands for metalanguage

Metalanguage

Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...

: it was conceived to develop proof tactics in the LCF theorem prover

LCF theorem prover

Logic for Computable Functions is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others in 1972. LCF introduced the general-purpose programming language ML to allow users to write theorem-proving tactics. Theorems in the system...

 (whose language, pplambda, a combination of the first-order predicate calculus and the simply typed polymorphic lambda calculus

Lambda calculus

In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...

, had ML as its metalanguage).