Robin Milner

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.

  • The Definition of Standard ML, Revised Edition

    The Definition of Standard ML, Revised Edition

    Robin Milner, Robert Harper, David MacQueen, and Mads Tofte

    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 the language, including users and implementers. Because computer programs are increasingly required to withstand rigorous analysis, it is all the more important that the language in which they are written be defined with full rigor. One purpose of a language definition is to establish a theory of meanings upon which the understanding of particular programs may rest. To properly define a programming language, it is necessary to use some form of notation other than a programming language. Given a concern for rigor, mathematical notation is an obvious choice. The authors have defined their semantic objects in mathematical notation that is completely independent of Standard ML. In defining a language one must also define the rules of evaluation precisely—that is, define what meaning results from evaluating any phrase of the language. The definition thus constitutes a formal specification for an implementation. The authors have developed enough of their theory to give sense to their rules of evaluation. The Definition of Standard ML is the essential point of reference for Standard ML. Since its publication in 1990, the implementation technology of the language has advanced enormously and the number of users has grown. The revised edition includes a number of new features, omits little-used features, and corrects mistakes of definition.

  • Commentary on Standard ML

    Robin Milner and Mads Tofte

    The full mathematical description of the functional programming language ML was given in Milner, Tofte, and Harper's Definition of Standard ML. This companion volume explains in depth the meaning, or semantic theory, of ML. Together, the two volumes provide a complete understanding of the most prominent of a new group of functional programming languages that includes Haskell and Scheme.In making the Definition easier to understand, the authors not only explain what ML is, they explain why it is. They present some of the rigorous analysis that supports the Definition including a selection of theorems that express important properties of the language. The Commentary is also a working document that shows the way in which the specialized theory of ML can contribute to broader research on language design and semantics.

    Contents Preface • Executing a Simple Program • Dynamic Semantics for the Core • Dynamic Semantics for the Modules • Static Semantics for the Core • Type Declarations and Principality • Static Semantics for the Modules • Signature Matching • Elaboration of Functors • Admissible Semantic Objects and Proofs • Elaboration of Signature Expressions • Principal Signatures • Appendixes: Proof of Principality • Identifier Status • Solutions to Exercises • Mistakes and Ambiguities

    • Hardcover $42.00
    • Paperback $21.00
  • The Definition of Standard ML

    Robert Harper, Robin Milner, and Mads Tofte

    This book presents the official, formal definition of the programming language ML including the rules for grammar and static and dynamic semantics. ML is the most well-developed and prominent of a new group of functional programming languages. On the cutting edge of theoretical computer science, ML embodies the ideas of static typing and polymorphism and has also contributed a number of novel ideas to the design of programming languages.

    Contents Syntax of the Core • Syntax of Modules • Static Semantics for the Core • Static Semantics for Modules • Dynamic Semantics for Modules • Programs

    Appendixes: Derived Forms • Full Grammar • The Initial Static Basis • The Initial Dynamic Basis • The Development of ML

    • Hardcover $30.00
    • Paperback $15.00

Contributor

  • The Little MLer

    The Little MLer

    Matthias Felleisen and Daniel P. Friedman

    Over the past few years, ML has emerged as one of the most important members of the family of programming languages. Many professors in the United States and other countries use ML to teach courses on the principles of programming and on programming languages. In addition, ML has emerged as a natural language for software engineering courses because it provides the most sophisticated and expressive module system currently available.Felleisen and Friedman are well known for gently introducing readers to difficult ideas. The Little MLer is an introduction to thinking about programming and the ML programming language. The authors introduce those new to programming, as well as those experienced in other programming languages, to the principles of types, computation, and program construction. Most important, they help the reader to think recursively with types about programs.