Also see the ML Manual for Nuprl4.

next up previous contents index
Next: Functional Style Up: The Metalanguage Previous: The Metalanguage

An Overview of ML

This section gives a brief summary of the features of ML. For a complete account the reader is referred to the book Edinburgh LCF [Gordon, Milner, & Wadsworth 79]. Originally, ML was developed as the metalanguage for the LCF proof system; several dialects of the language have since evolved, including Cambridge ML, the implementation of ML used in Nuprl . The ML used in Nuprl differs in several minor ways from the original ML, for we have specialized the language to the Nuprl logic.

The principal  features of ML are:

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995