ML (Meta Language) is the metalanguage developed for the Edinburgh LCF theorem prover in the 1970s. It is an early statically typed, functional language with polymorphic type inference in the Hindley–Milner style, and other features like exceptions and mutable variables.
History
ML started development by Robin Milner upon his arrival at University of Edinburgh in 1973 with the help of research assistants Lockwood Morris and Malcolm Newey, both postdocs from Stanford who were hired by Milner. Michael Gordon, Christopher Wadsworth, and other graduate students joined in research by 1975. The design of the first version of ML was finalized, and subsequently documented in the 1979 book Edinburgh LCF by Milner along with Gordon and Wadsworth. This version of the LCF was subsequently updated to use an early version of Standard ML, and has been uploaded to GitHub.
With the attention and excitement around ML, LCF, and other related technologies at the time, such as the contemporaneous programming language Hope, happening subsequent to the release of Edinburgh LCF and other developments at the time, a meeting was convened with the title "ML, LCF, and Hope" in November 1982. Concerns with the splintering of both design and implementation leading to duplicated work was raised in this meeting. Although Milner seemed open to the spirit of experimentation in the meeting, further discussions and meetings were had between Bernard Sufrin and Milner, where Sufrin urged Milner to unify the design of ML. These correspondences were later referenced in the second draft of Milner's proposal for Standard ML.