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. [Coming soon, a page about process calculi, action calculi and BPM.]

Read a paper about the Pi Calculus breakthrough and Business Processes

Read an interview with Robin Milner

 

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. I would like to outline my research work under two headings: first, an experience in formally defining a programming language; second, and more fully, a descriptive calculus of communicating systems.

 

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.