The Definition of Standard Ml

Standard ML is a general-purpose programming language designed for large projects.This book provides a formal definition of Standard ML for the benefit of all concerned with thelanguage, including users and implementers. Because computer programs are increasingly required towithstand rigorous analysis, it is all the more important that the language in which they arewritten be defined with full rigor.One purpose of a language definition is to establish a theory ofmeanings upon which the understanding of particular programs may rest. To properly define aprogramming language, it is necessary to use some form of notation other than a programminglanguage. Given a concern for rigor, mathematical notation is an obvious choice. The authors havedefined their semantic objects in mathematical notation that is completely independent of StandardML.In defining a language one must also define the rules of evaluation precisely--that is, definewhat meaning results from evaluating any phrase of the language. The definition thus constitutes aformal specification for an implementation. The authors have developed enough of their theory togive sense to their rules of evaluation.The Definition of Standard ML is the essential point ofreference for Standard ML. Since its publication in 1990, the implementation technology of thelanguage has advanced enormously and the number of users has grown. The revised edition includes anumber of new features, omits little-used features, and corrects mistakes of definition.

Robin Milner was Professor Emeritus of Computer Science at the University of Cambridge, UK, and Professor at the Informatics Forum in the University of Edinburgh.