分享

Robin Milner( 1934–)

图灵奖获得时间：

1991年。 第二十六位图灵奖(1991年)获得者。

图灵奖引用(Turing Award 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图灵奖以表彰其在) 三个研究领域的杰出的和完整性的成就：

1. LCF, 一个(Dana Scott)的可计算函数逻辑(Logic of Computable Functions)的实现机制，(可能)是第一个理论上和实践上都具备的计算机证明(数学)定理的工具。

2. ML, 第一个具有多态的类型推理和具有安全类型的异常处理机制的(编程)语言。

3. CCS, 一个并发系统的综合理论。

另外，Robin Milner在operational 和denotational的语义关系方面进行了形式化的描述和深入的研究。

笔者注：

LCF: Logic of Computable Functions.

http://en.wikipedia.org/wiki/LCF_theorem_prover

http://en.wikipedia.org/wiki/Automated_theorem_proving

ML:

http://en.wikipedia.org/wiki/ML_programming_language

CCS: Calculus of Communication Systems

http://en.wikipedia.org/wiki/Calculus_of_Communicating_Systems

CSP(Communicating Sequential Processes)是另外一个著名的描述并发系统的形式语言，

由CAR Hoare(1980年图灵奖得主) 发明.

CSP: http://en.wikipedia.org/wiki/Communicating_sequential_processes

另外一个著名的时序逻辑描述语言是LOTOS.

LOTOS (Language Of Temporal Ordering Specification):

http://en.wikipedia.org/wiki/LOTOS

关于并发系统，可参见：http://vl.fmnet.info/concurrent/
A Brief History of Process Algebra
Some Thoughts on Specification: http://research.microsoft.com/users/lamport/tla/notes/92-05-05.txt
Modelling Concurrent Systems – Lecture

Turing Award Lecture(图灵奖演讲文章)：

Elements of Interaction – Turing Award Lecture. Commun. ACM 36(1): 78-89(1993)
Robin Milner简介:

Robin Milner于1934年出生于Plymouth, 英国。1952年，Milner毕业于剑桥大学King学院( http://www.kings.cam.ac.uk/)。

剑桥大学毕业后，Milner先后就职于Ferranti公司，伦敦城市大学，Swansea大学，斯坦福大学。1973年，就任与University of Edinburgh (http://www.ed.ac.uk/ ). 1995年，Milner回到剑桥大学计算机实验室(Computer Laboratory: http://www.cl.cam.ac.uk/  )出任教授。另外除了LCF，ML和CCS的杰出贡献之外，Milner也是pi-calculus的发明者之一。

关于pi-calculus，可参见：http://en.wikipedia.org/wiki/Pi-calculus
“In theoretical computer science, the π-calculus is a notation originally developed by Robin Milner, Joachim Parrow and David Walker as an advance over Calculus of Communicating Systems in order to provide mobility in modeling concurrency. The π-calculus is in the family of process calculi that have been used to model concurrent programming languages just as the λ-calculus has been used to model sequential programming languages.”
Robin Milner在剑桥大学的主页: http://www.cl.cam.ac.uk/users/rm135/
Robin Milner Wiki: http://en.wikipedia.org/wiki/Robin_Milner

Robin Milner照片:

 

分享