Robin
Milner
Also see a page about Pi-calculus
Robin Milner was
appointed Professor of Computer Science at Cambridge UK in 1995, and was Head
of the Computer Laboratory there from January 1996 to October 1999. Before
that he spent two years in the Artificial Intelligence Laboratory at
Stanford University, then 22 years in the Computer Science Department at the
University of Edinburgh, where in 1986 he and colleagues founded the Laboratory
for Foundation of Computer Science. He was elected Fellow of the Royal Society
in 1988, and in 1991 he gained the A.M. Turing Award.
From 1971 to 1980,
at Stanford and Edinburgh, he worked on computer-assisted reasoning; with
colleagues he developed LCF (Logic for Computable Functions), a system for
machine-assisted formal reasoning. This was a model for several later systems.
He led a team which designed and defined Standard ML, a widely used programming
language and one of the first industry-scale languages whose semantic definition
is fully formal.
His main work has been in the theory of concurrent computation. Around 1980 he developed CCS (Calculus for Communicating Systems), one of the first algebraic calculi for analysing concurrent systems. In the late 1980s with two colleagues he devised the pi calculus, a basic model for mobile communicating systems. These calculi are part of a continuing quest for a theory which unites computing and communication. Some of this work is widely accessible through his book "Communication and Concurrency" (1989) and "Communicating and Mobile Systems (1999).
Robin Milner on Process Calculus and Business Processes
“I'm delighted that Business
Process Management (BPM) and its modeling language, BPML, have found good
use for the concepts of process calculus. For over two decades the process
calculus community has sought to combine two things: the way you define and
analyze mobile distributed processes and the way you program them. We believe
we've found the basic maths to meet this challenge, and it is heartening to
hear that it is being applied to the management and automation of a company's
most basic economic assets, its core processes. For computer scientists, the
practical observation of the use of process calculus within the IT industry's
newest software category, the Business Process Management Systems (BPMS),
will help us to deepen our theories, particularly in terms of higher level
process representation. We aim not just to build, but to understand, the colossal
global computer in which we live. It is exciting that business systems can
now not only use what we have done so far, but will also help us to come closer
to our goal.” Robin Milner, November 2002
ACM Citation
For three distinct and
complete achievements: 1) LCF, the mechanization of Scott's Logic of Computable
Functions, probably the first theoretically based yet practical tool for
machine assisted proof construction; 2) ML, the first language to include
polymorphic type inference together with a type-safe exception-handling
mechanism; 3) CCS, a general theory of concurrency. In addition, he formulated
and strongly advanced full abstraction, the study of the relationship between
operational and denotational semantics.
Robin Milner
receives 1991 Turing Award
From the LFCS
Newsletter, Autumn 1991, Issue 5.
It is a great pleasure to record that Professor Robin Milner FRS, the first director of LFCS, is to receive the 1991 A.M. Turing Award. This is the highest honour of the Association of Computing Machinery; indeed it is fair to say that it is the highest honour in Computer Science. The award will be formally presented to Professor Milner in Kansas City in March when he gives the Turing Lecture there. The Turing Award has been in existence since 1966, when the first recipient was Alan J. Perlis. Others include Stephen A. Cook, Edsgar W. Dijkstra, C. Anthony R. Hoare, Richard M. Karp, Donald E. Knuth, John McCarthy, Marvin Minsky, Dana S. Scott and Nicklaus Wirth.
The citation makes plain the wide-ranging and influential nature of Robin Milner's work:
“Working in
challenging areas of Computer Science for twenty years, Robin Milner has the
distinction of establishing an international reputation for three distinct
and complete achievements, each of which has had and will continue to have
a marked, important and widespread effect on both the theory and practice
of Computer Science:
1. LCF, the
mechanisation of Scott's Logic of Computable Functions, probably the first
theoretically based yet practical tool for machine-assisted proof construction.
2.ML, the first
language to contain polymorphic type inference together with a type-safe
exception handling mechanism. The type-inference algorithm applied to a full
language is a major theoretical advance.
3. CCS, a
general theory of concurrency.
In addition
he formulated and strongly advanced full abstraction, the study of the relationship
between operational and denotational semantics. A key ingredient in all of his work has
been his ability to combine deep insight into mathematical foundations of
the subject with an equally deep view of the key engineering issues, thus
allowing the feedback of theory into practice in an exciting way. Further,
his style of scholarship, rigour and attention to æsthetic quality sets a
high example for all to follow.”
The first two parts
of Robin's work are intimately linked. In the course of the LCF work, ML was
developed as a "meta-language" for expressing and manipulating logical
proofs. The most recent embodiment of the language was in the design of Standard
ML. The design team which Robin led won the 1987 British Computer Society
Award for Technical Achievement.
The work in concurrency
is rather independent of both of these. Currently, Robin is an SERC Senior
Research Fellow and most of his energies are going into concurrency. It is
an aim of his there to find a foundation for concurrency as basic as the lambda
calculus is for sequential computation. His pi-calculus is intended to be
a step in this direction.
Robin's foundational
approach to concurrency reveals, I think, the kind of insight described at
the end of the citation. The task of finding such a foundation is intimately
linked with that of finding a theory unifying sequential and concurrent computation.
Robin's work on the pi-calculus can be viewed as an important contribution.
Congratulations to Robin, and may the future prove as fertile for him as has
the past!
Speech by Robin
Milner on receiving an Honorary Degree from the University of Bologna
Outline
I am deeply honoured
to receive the Degree that has been conferred on me.
I would like to
spend a few minutes talking about the way that computer science is developing
from a study of tools for computation into a broad science of interactive behaviour,
and I shall illustrate it with my own work which is very much a part of the
development.
My research in computing
has been always concerned with language. I don't mean natural language, but
the more formal language which we use in controlling and analysing discrete
dynamic systems - in other words, in controlling computers.
Every tool designed
by man is a prosthetic device, and for every prosthetic device there is a
means of control. Many tools are physical, and their control is manual. In
contrast, computers are the most complex tools ever invented, and they are
tools of the mind; the means of control is hardly muscular - it is primarily
linguistic. Quite simply, the versatility of computers is exactly equal to
the versatility of the languages by which we prescribe their behaviour, and
this appears to be unbounded.
But computing is
not only about a computer's internal action; it is about the way a computer
behaves as part of a larger system, say an aircraft. It follows that the terms
in which the computer behaviour is prescribed must harmonize with the
way we describe information flow in such systems. Thus computing expands
into informatics, the science of information and communication.
I am deeply aware
of the long tradition on mathematics at this famous university; I am also
impressed by the fact that Marconi, the pioneer of radio communication, is
from Bologna. So it is appropriate in this place to propose a new way in which
mathematics can inform the study of communication.
Programming language
as a model
For a decade and
a half, from 1975 to 1990, I worked with an large team of people on a project
whose goal was as follows: Define an extremely powerful language for programming
which not only encourages people to write correctly, but whose meaning is
defined completely and lucidly by mathematics, not by a users' manual.
The aim of this
work was to be sure that we really understand the tool we use for programming.
The reason for wanting to understand it is rather obvious; if we don't understand
it then the programs we write will have an unclear meaning. Language is the
raw material of software engineering, rather as water is the raw material
for hydraulic engineering. The difference is that water is rather well understood
by physical science; but software - as a raw material - is still not scientifically
understood. Nevertheless our software engineers have filled the world with
software at enormous speed. So it is perhaps not surprising that we have a
software crisis of staggering proportions, in which it is estimated that 80%
of programming time is spent trying to understand old computer programs to
bring them up-to-date with the tasks they perform! With the enormous demand
for computing applications, people who wrote programs left no time to explaining
how they worked - and it still goes on.
The language my
team developed was called Standard ML; it is now quite widely used in applications,
very widely used in teaching, and is probably the first language which is
large enough for heavy-duty application and yet has been fully defined by
mathematical means. Time forbids me to tell you its the details. But because
it was defined mathematically, it can also be analysed mathematically. Indeed,
we proved several theorems which demonstrate that certain kinds of bad behaviour,
i.e. certain kinds of programming fault or bug, can never occur in a well-formed
program in the language.
We did not design
the perfect language - that does not exist. But I believe that the Standard
ML project sets a standard for how computing languages should be conceived;
not just as syntactic conventions for assembling millions of lines of code,
but as the expression of dynamic mathematical models.
Models of communicating
systems
I would now like
to turn to my other and greatest excitement, trying to understand how discrete
systems communicate with each other.
For twenty-five
years I have been trying to merge programming, the prescriptive or synthetic
activity, with the task of description or analysis in computing.
The latter becomes more important as we move towards systems which interact
with each other.
This interaction
is ubiquitous. It occurs between the component parts of a single computer,
e.g. between the processor and the memory; it occurs between the computers
in an aircraft and the aircraft components which they control; and now, overwhelmingly,
it occurs on the Internet.
My Calculus of Communicating
Systems, published in 1980, aims to describe and analyse systems such systems.
One of its many applications has been in the analysis of so-called communications
protocols - ways of ensuring that information is correctly transmitted
even through unreliable media. Another was the software which monitors behaviour
in a nuclear power plant.
Nearly ten years
ago, with colleagues Joachim Parrow and David Walker and based upon ideas
from Mogens Nielsen and Uffe Engberg, I extended the calculus and gave it
a snappier name: the pi-calculus. We had noticed that the most challenging
and intractable problem, which we had not fully addresses was the mobility
of interactive systems - the way in which pieces of information and even active
computer programs (applets, or viruses) move from one machine to another and
make themselves useful (or harmful) in a new environment. At that time, the
Internet was a dream in someone's mind, but the reality we now have is not
so far from our theoretical conception of mobile informatic systems.
Thus, while Standard
ML is a synthetic language, for building systems, the pi-calculus is
an analytical tool for understanding them. This is why we call it a
``calculus''. We dare to use this word by analogy with Leibnitz's differential
calculus; the latter - incomparably greater - is based upon continuous mathematics,
while the pi-calculus is based upon algebra and logic; but the goal in each
case is analysis, in one case of physical systems and in the other
case of
informatic systems.
Moreover, we found
that the pi-calculus may be significant in a way which we did not fully expect.
We are very familiar with basic models of computation; for example,
most scientists have heard of Alan Turing's famous ``Turing Machine'', a very
simple device on which anything that's computable can be computed. Is there
such a basic model for all discrete interactive behaviour? We don't
yet know how to pose this question precisely, but we think of the pi-calculus
as a tentative step towards such a model.
Conclusion
With this congruence
between computing and interaction in mind, I would like to end with a prediction
which should now not seem absurd. I believe that computer science or informatics,
which began as just the engineering of scientific and business calculations,
has broadened into a descriptive science with enormous breadth of application,
not just to computation but to dynamic systems in general. By giving a structural
account - to complement Shannon's quantitative account - of information flow,
it can provide an exact view of the world which is not the province of any
previously existing science.