Robin Milner

Robin Milner

[Peter Freyd]

                 Copyright 2001 TSL Education Limited
                The Times Higher Education Supplement

                           February 2, 2001

SECTION: COMPUTING; BOOKS; No.1472; Pg.26

LENGTH: 1616 words

HEADLINE: Honouring The Master Of Logical Languages

BYLINE: Jonathan Bowen

BODY: Proof, Language and Interaction Edited by Gordon Plotkin, Colin
Stirling and Mads Tofte MIT Press, 722pp, Pounds 48.50 ISBN 0 262
16188 5 THES Bookshop Pounds 44.50 Tel: 020 8324 5104

This Festschrift, or celebratory publication, honours an important
contributor to the fundamentals of computer science. Robin Milner, to
whom this volume is dedicated, has been a cornerstone of the
theoretical computer science world for the past three decades or so.

The book begins with an enlightening biography of Milner's
professional achievements that helps set the context for the rest of
the book. As is usual in a Festschrift, the volume mainly consists of
contributions from Milner's immediate colleagues and those working in
the same field on related topics. All the contributions are of
international stature and are largely technical in nature. Thus, this
book provides an important in-depth snapshot of the work of some of
the best minds in the area of theoretical computer science.

Milner had an excellent education. He won a scholarship to King's
College, Cambridge, in 1952 - the same college where Alan Turing had
won a similar scholarship about 20 years earlier. He studied
mathematics, the underpinning of computer science, and, for a while,
Cambridge's "moral sciences", or philosophy in normal parlance.

The early professional experiences of Milner were as a schoolteacher
and as a programmer at Ferranti, both useful grounding for a computer
science academic. He then worked at City University in London, Swansea
University, Stanford University in California and, from 1973, at
Edinburgh University, where his most important work was undertaken.

In 1995 he moved back to Cambridge, where he now heads the Computer
Laboratory. He has received the highest awards, including a fellowship
of the Royal Society in 1988 and the annual ACM Turing Award in 1991,
computer science's nearest equivalent to a Nobel prize.

Milner's contributions to theoretical computer science have been in
the areas of programming language semantics using domain theory,
computer-assisted theorem proving, the programming language ML
(standing for "Metalanguage") and, perhaps most significantly,
concurrency. His early influences included Christopher Strachey
(leader of the Programming Research Group at Oxford and originator of
denotational semantics), Rod Burstall (also at Edinburgh), Peter
Landin (a free-spirit pioneer of computing), Dana Scott (who worked
with Strachey at Oxford on the foundations of programming languages)
and John McCarthy (of artificial intelligence fame at Stanford, who
coined the term AI).

At Stanford, Milner developed the Stanford LCF (logic of computable
functions) while working within McCarthy's AI group, based on a logic
developed by Scott using a typed l-calculus (the essential underlying
theoretical basis for the functional programming paradigm). This
subsequently developed into Edinburgh LCF, with its own programming
language Edinburgh ML that was designed to aid in the discovery and
construction of proofs, an inspired idea for the time. This became
Standard ML that, because of its carefully designed and well-
understood formal semantics, has proved to be an excellent, more
general programming language.

If the above efforts are not enough, probably Milner's most important
contribution concerns the formal underpinning for concurrency,
starting with his calculus of communicating systems (CCS). This
introduced the notion of bisimulation for comparing the equivalence of
processes. Although an influential concept, some researchers have
considered bisimulation too restrictive in practice (for example, in
strong bisimulation, both processes must execute the same number of
steps) and Milner himself proposed a more forgiving weak bisimulation.

CCS has always been somewhat in competition with Tony Hoare's
communicating sequential processes (CSP) in terms of influencing the
field, with the usual camps of researchers expert in each. However,
more recently Milner has developed his ideas further with a newer
p-calculus for mobile computing that is increasingly important in
practical terms with the development of the internet. Milner remains
active in this area.

Milner's influence on his field is significant, as the contributions
in this book attest. Many subsequent theorem provers produced by other
researchers have been inspired by Milner's original LCF, including the
development of Cambridge LCF, and the related HOL (higher order logic)
by Mike Gordon, as well as Isabelle by his colleague Larry Paulson
(both contributors to this book). ML has also been developed further
and other theorem-proving systems like Coq, Lego and NuPrl owe much to
Milner's ideas.

Proof, Language and Interaction is divided into five sections:
"Semantic foundations", "Programming logic", "Programming languages"
and "Concurrency and mobility". These successfully reflect the
developing interests of Milner through his professional career.

"Semantic foundations" includes contributions on the linking of
different types of semantics. Full abstraction, a term coined by
Milner, is developed further by Samson Abramsky, a colleague at
Edinburgh who has since moved on to join the Programming Research
Group (PRG) at Oxford within the Oxford University Computing
Laboratory. Hoare, who recently moved from the PRG to join Microsoft
Research in Cambridge, is closely associated with the Computing
Laboratory there. He presents his and his colleagues' work on
deriving an operational semantics algebraically. The linking of
semantics and concurrency is also explored.

In "Programming logic", Gordon (like Milner, of Edinburgh and
Cambridge) gives a helpful and less technical historical view of the
development of the original LCF into his own important contribution to
computer science, HOL, one of the most widely used theorem provers.
Paulson, colleague at Cambridge, gives a related but much more
technical account of a fixed-point approach to induction. Robert
Constable, developer of the NuPrl theorem prover, and his colleagues
at Cornell University in the United States, present the formalisation
of automata theory.

The "Programming languages" section naturally includes work on
Milner's ML as well as a programming language based on the
p-calculus. Gerard Berry, who is based in Paris, presents a useful
introduction to the important synchronous language Esterel, whose
design was highly influenced by Milner's work on process calculi and
bisimulation.

The section on concurrency, as expected, includes developments of
Milner's CCS. The final mobility section presents advances with
respect to the p-calculus, which is where Milner's most recent
research interests and contributions lie.

All of these essays build on concepts that Milner originated or
promulgated himself, either directly or indirectly. This unifying
force helps to provide structure to the book, especially because
Milner's own work, although it is varied in application, has a
consistency in elegance of style that is a feature of work by all
top-class theoreticians.

The book finishes with a list of contributors, but does not include an
index. This would have been a useful addition for those wishing to use
it as a reference work. Some abbreviations (for example PCF, a
programming language development of LCF) are introduced without
expansion or comprehensive explanation. An index might have made some
of these omissions clear to the editors. Alternatively, or in
addition, a glossary of terms, especially those coined by Milner
himself, would have been an interesting supplement. However, these are
minor quibbles in an otherwise well-edited and presented volume.

The majority of the material is highly technical in nature and is only
suitable for those acquainted with the field. The introductory
biography is naturally approachable to a wider readership and is a
useful historical record, but its 17 pages, out of a voluminous 722 in
total, would not alone justify acquisition of the book. Ultimately,
this collection will be at home in any good computer-science library,
and this will probably be its main destination. It will also be of
interest to theoretical computer scientists wanting a book that
provides a range of invited papers all of which are of international
journal class. Most computer scientists with an interest in the
theoretical developments of the subject would be only too happy to
have this book on their shelves if they could afford it.

In 1999, as head of the Computer Laboratory at Cambridge, Milner
officiated during the celebrations for the 50th anniversary of the
early Edsac computer, developed by Maurice Wilkes and his team, which
first ran a program successfully in 1949. Indeed, in 1956, Milner
himself attended a computing course at Cambridge using the Edsac.
Wilkes was a important leader of the Cambridge University Computer
Laboratory. His expertise on the pioneering practical development of
computers counterpoints Milner's contribution in the mathematical
underpinning of computer science.

The balance of theory and practice has been a key feature of work
undertaken at Cambridge that continues under Milner's direction to
this day and is the basis for all significant computer-science
research. Milner has always ensured that his research contributions
have been relevant as well as fundamental.

This book is a fitting "thank you" from those who have benefited most
directly from Milner's insights. In turn, it should help others to
appreciate his influential contribution to theoretical computer
science.

Jonathan Bowen is professor of computing, South Bank University.