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:

• a functional style including the ability to use functions as values;
• a mechanism allowing the definition of new (abstract) data types;
• a polymorphic type discipline; and
• an exception--trap mechanism.

• Functional Style
• Type Definitions
• Polymorphic Typing
• Failures
• Syntax and Semantics
• Using ML in Nuprl