Mads Tofte

Mads Tofte is Vice Chancellor, IT University of Copenhagen.

  • Proof, Language, and Interaction

    Proof, Language, and Interaction

    Essays in Honour of Robin Milner

    Gordon Plotkin, Colin P. Stirling, and Mads Tofte

    This collection of original essays reflects the breadth of current research in computer science.

    This collection of original essays reflects the breadth of current research in computer science. Robin Milner, a major figure in the field, has made many fundamental contributions, particularly in theoretical computer science, the theory of programming languages, and functional programming languages. Following a brief biography of Milner, the book contains five sections: Semantic Foundations, Programming Logic, Programming Languages, Concurrency, and Mobility. Together the pieces convey a seamless whole, ranging from highly abstract concepts to systems of great utility.

    Contributors Samson Abramsky, J. C. M. Baeten, Sergey Berezin, J. A. Bergstra, Gérard Berry, Lars Birkedal, Gérard Boudol, Edmund Clarke, Pierre Collette, Robert L. Constable, Pierre-Louis Curien, Jaco de Bakker, Uffe H. Engberg, William Ferreira, Fabio Gadducci, Mike Gordon, Robert Harper, Matthew Hennessy, Yoram Hirshfeld, C. A. R. Hoare, Gérard Huet, Paul B. Jackson, Alan S. A. Jeffrey, Somesh Jha, He Jifeng, Cliff B. Jones, Cosimo Laneve, Xinxin Liu, Will Marrero, Faron Moller, Ugo Montanari, Pavel Naumov, Mogens Nielsen, Joachim Parrow, Lawrence C. Paulson, Benjamin C. Pierce, Gordon Plotkin, M. A. Reniers, Amokrane Saïbi, Augusto Sampaio, Davide Sangiorgi, Scott A. Smolka, Eugene W. Stark, Christopher Stone, Mads Tofte, David N. Turner, Juan Uribe, Franck van Breugel, David Walker, Glynn Winskel

  • 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