悼念图灵奖得主、ML语言之父Robin Milner

【引文】

在上编译工程时第一次接触函数程式语言，立刻就被其简单的数学逻辑给迷住了。

现在有空就会看看LISP和SML的资料，希望能够对其的研究更近一步，一边学习一边对其在IT界的地位产生了很大的好奇，两种语言的作者无疑都因为此而获得了图灵奖，这是除了C之外其他语言没有享受过的殊荣，连Java、Python、Perl 这些现在热捧的语言也没有过。

由此可知ML这种语言在编程语言中的地位不一般，今晨获知其作者前几日离世，故此希望发文悼念之，缅怀其丰功伟绩。



1991年图灵奖得主Robin Milner于2010年3月20日（他妻子葬礼后的第三天）在英国剑桥辞世，享年76岁。他是他是英国皇家学会成员，ACM会士，美国工程院外籍院士。

生平

Robin Milner出生于一个军人家庭，早年就读于伊顿公学。后加入英国皇家工程兵部队，获得少尉军衔。1952年入读剑桥大学国王学院，1957年毕业，之后的第一个工作是教师，然后在Ferranti公司当程序员。此后他进入学术界，先后在伦敦城市大学，Swansea大学，斯坦福大学任职。1973年回到英国爱丁堡大学，在爱丁堡大学任职期间，他开发了函数式编程语言ML，并和他的同事一起完成了LCF的开发。1995年，他回到母校剑桥大学任教，并担任剑桥大学计算机实验室主任。（来自维基百科）

2005年4月Milner曾经访问中国。

去世前，他的主要研究兴趣是模型在普适计算中的系统应用，和偶图（Bigraphy）模型。

贡献

他获得图灵奖的主要贡献是：

1. LCF，Scott可计算函数逻辑（Logic of Computable Functions）的机械化，可能是第一个基于理论但实用的计算机辅助证明工具。

2. ML，第一个具有多态的类型推演和具有类型安全异常处理机制的编程语言。其设计目的就是为了进行LCF证明。这是一个通用的函数式语言，对语言设计的最大贡献是Hindley-Milner类型推演算法，用于许多静态语言。ML是Caml、Haskell、F#等语言的先祖。

3. CCS，一个并发的通用理论。

另外，他提出并发展了完全抽象，研究了操作语义和指称语义之间的关系。

轶事

在一次访谈中，Milner 说到自己早年在剑桥上学时，根本不知道图灵及其成就。虽然他进剑桥国王学院时，学院的院士之一图灵刚刚去世几个月，虽然他的数学老师是图灵的好友。他在大学喜欢的是罗素的分析哲学。毕业的时候虽然很多人劝他留在学校，他还是走了。更有意思的是，当时有一堂EDSAC（早期计算机之一）编程课，却让他对编程产生了厌恶之情。而在中学当了一年老师之后，他却不得不违心找了一份程序员的工作。

他真正对计算机产生兴趣，还是在伦敦城市大学的时候，他对与分析哲学很密切的人工智能着了迷，并学习了C语言的先祖CPL，后来又因为研究数据库学习了关系代数。

他有一个没有完成的梦想，是成为一名音乐家。事实上，他大学期间主要精力都花在音乐上了，他是一名非常出色的双簧管演奏家。