Interview With Turing-Award Winner Robin Milner

Martin Berger 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. 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 here."

Comments

So he's the one

[bsharitt]

So he's the reason I have to take so much calculus to be a computer programmer.

Ok, here we go

[October_30th]

"He may not be as well-known as he deserves to be, but his research contributions are ubiquitous"

Now that just makes feel so much more confident about his work...

How do we know?

[guacamolefoo]

How do we know that the interview is with the Turing Award winner? Maybe the interview was just with a computer?

GF.

Obligatory disclaimer for the Comic Book Guys out there:
I know, I know -- the Turing Prize isn't the Loebner Prize. It's the day before a holiday -- give it a rest and laugh a little.

Still a male-dominated industry...

[Space cowboy]

Coq and Isabelle are used heavily "for verification purposes" today. ... poor old Isabelle... Give a girl a break!

Simon.

Re:So he's the one tsarkon reportst

[Anonymous Coward]

so even with the help of a computer your dumb ass is whining about learning math that newton and Leibniz discovered in the late 1600's.

get with the times. (there is evidence that archimedes understood infinity much more than realized before with new evidence, and he lived in 225 BC. )

care to whine about calculus anymore?

Re:Formal proofs?

[heironymouscoward]

You're an ignorant bastard and you should RTFA instead of spouting your half-cooked opinions.

(Help, moderators, mod me "-1 Insane in the membrain", I'm flaming myself!)

Re:Formal proofs?

[Anonymous Coward]

This is the strangest instance of Karma-Whoring I have ever seen. Congrats, I think...