Home
 

Robin Milner receives 1991 Turing Award

by Gordon Plotkin

From the LFCS Newsletter, Autumn 1991, Issue 5.

Robin Milner

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!