Berger continues "There is
also a direct line from this strand of Milner's work to what may be
one of the hottest topics in computer science: proof
carrying code. Milner also headed the effort to develop ML (best known today by its
descendant Ocaml), the first language to
include polymorphic type inference together with type-safe
exception-handling and module mechanisms. Most modern programming
languages can trace some of their advanced features directly back to
ML's pioneering efforts. Most of all, he established concurrency
theory as a scientific field by creating and studying idealised
concurrent programming languages like the Pi-Calculus. That
calculus is becoming more and more influential in the design of new
programming languages (for example Microsoft's XLANG) and the WWW infrastructure.
A few weeks ago, I interviewed
Milner. I wanted to find out about the man and the stories behind all
this great research. I hope you find it as interesting as I do.
The transcript of the interview can be found
writes "Turing Award
(1991) winner Robin
Milner is one of the most influential computer scientists. He may
not be as well-known as he deserves to be, but his research
contributions are ubiquitous: he developed the first mathematically
sound yet practical tool for machine assisted proof construction. This
research has been continued successfully and led to many useful proof
assistants such as HOL, Coq or Isabelle
that are being used heavily for verification purposes today."
Read on for more information about Milner, and a link to Berger's excellent interview with him.