[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article

Review of proof, language, and interaction: essays in honour of Robin Milner edited by Plotkin, Stirling and Tofte

Published: 01 March 2001 Publication History

Abstract

The field of theoretical computer science has had a long tradition of providing wonderful edited books to honor various prominent members of the community. The idea behind such edited works is clear: celebrate the work of a particular researcher by having co-authors and colleagues write papers on subjects related to the researcher's body of work. When successful, such a project provides for a wonderful excursion through the work of a researcher, often highlighting an underlying coherence to that work.On that account, the book Proof, Language, and Interaction: Essays in the Honor of Robin Milner (edited by Plotkin, Stirling and Tofte) is a success. In no small part this is due to Milner's span of work from theory to practice. It is hard to both briefly describe Milner's contributions and give an idea of the breadth of his effort. Two major tracks of research emerge. First, after some work with John McCarthy's AI group at Stanford, he developed LCF (specifically, Edinburgh LCF), a system for computer-assisted theorem proving based on Dana Scott's idea on continuous partial functions for denotational semantics. Not only working on the implementation, Milner also worried about the semantic foundations [1]. LCF came with a programming language, Edinburgh ML, which evolved with Milner's help into standard ML, a higher-order language that introduced many features now standard in advanced programming language, features such as polymorphism and type inference [4]. His second track of research involves concurrency. He invented CCS, the calculus of communicating systems [2]. Work on the semantics of CCS went from the traditional domain-theoretic approach to a new operational view of processes equality based on the notion of bisimulation. Subsequent work by Milner led to the development of other calculi, most notably the π-calculus, which included a powerful notion of mobility [3]. His later work in the area attempted to provide a unifying framework for comparing calculi, and unifying sequential and concurent computation.This range of interests is reflected in the table of contents of the book. The book splits across different subjects: semantic foundations, where we discover work aimed at understanding computation, both sequential and concurrent, programming logic, where we discover work derived from Milner's work on LCF, and aimed at understanding the role of formal mathematics, programming languages, where we discover Standard ML, and other languages based on Milner's idea about concurrent calculi, concurrency, where we discover work on Milner's early CCS approach and extensions, and mobility, where we discover work related to the π-calculus.

References

[1]
R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4:1-22, 1977.
[2]
R. Milner. A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer-Verlag, 1980.
[3]
R. Milner. Communicating and Mobile Systems: The π-calculus. Cambridge University Press, 1999.
[4]
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, Cambridge, Mass., 1997.
  1. Review of proof, language, and interaction: essays in honour of Robin Milner edited by Plotkin, Stirling and Tofte

        Recommendations

        Comments

        Please enable JavaScript to view thecomments powered by Disqus.

        Information & Contributors

        Information

        Published In

        cover image ACM SIGACT News
        ACM SIGACT News  Volume 32, Issue 1
        March 2001
        88 pages
        ISSN:0163-5700
        DOI:10.1145/568438
        Issue’s Table of Contents
        Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        Published: 01 March 2001
        Published in SIGACT Volume 32, Issue 1

        Check for updates

        Qualifiers

        • Article

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • 0
          Total Citations
        • 9
          Total Downloads
        • Downloads (Last 12 months)1
        • Downloads (Last 6 weeks)0
        Reflects downloads up to 23 Feb 2025

        Other Metrics

        Citations

        View Options

        Login options

        View options

        PDF

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        Figures

        Tables

        Media

        Share

        Share

        Share this Publication link

        Share on social media