From cat-dist@mta.ca Sat Feb 10 16:17:31 2001 X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 8 Feb 2001 08:29:53 -0500 (EST) From: Peter Freyd <pjf@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Robin Milner
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.