图灵奖：罗宾·米尔纳（1991）

图灵奖是计算机界最负盛名的奖项，有“计算机界诺贝尔奖”之称。”图灵奖”系列将介绍历届获奖者。每周二更新，本文为第 31 期。图灵奖：罗宾·米尔纳（1991）

文章来自微信公众号“科文路”，欢迎关注、互动。转发须注明出处。

本文来自 wiki:Robin Milner，翻译基于 谷歌翻译.

分时操作系统

亚瑟·约翰·罗宾·戈雷尔·米尔纳 FRS（Arthur John Robin Gorell Milner，FRS，1934 年 1 月 13 日 – 2010 年 3 月 20 日）是一位英国计算机科学家。

他于 1991 年获得图灵奖。

其图灵奖颁奖词为“获得三项独特且完整的成就：1. LCF，斯科特可计算函数逻辑的机制，可能是第一个基于理论且实用的机器辅助证明构建工具；2. ML，第一种包含多态类型推断和类型安全异常处理机制的语言；3. CCS，并发的一般理论。此外，他还提出并大力推进了完全抽象，即操作语义和指称语义之间关系的研究。”。（*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.*）

生平

米尔纳出生于英国普利茅斯附近耶尔普顿的一个军人家庭。

他就读于剑桥大学国王学院，并于 1957 年毕业。

米尔纳先是一名教师，然后在 Ferranti 担任程序员，之后进入伦敦城市大学、斯旺西大学、斯坦福大学的学术界，并从 1973 年开始在爱丁堡大学工作，他是计算机科学基础实验室 (LFCS) 的联合创始人。

1995 年，他回到剑桥，担任计算机实验室的负责人，但最终辞职。

自 2009 年起，米尔纳担任苏格兰信息学与计算机科学联盟高级研究员，并担任（兼职）爱丁堡大学计算机科学系主任。

米尔纳于 2010 年 3 月 20 日在剑桥因心脏病去世。

贡献

• LCF，Logic for Computable Functions
  • 最早的自动定理证明（Automated theorem proving, ATP）工具之一
• ML
  • 他为LCF开发的语言ML是第一个具有多态类型推断和类型安全异常处理的语言
• 通信系统演算(CCS)，$\pi$-演算
  • 分析并发系统的理论框架，即通信系统演算(CCS)及其继承者π演算

~~

都看到这儿了，不如关注每日推送的“科文路”、互动起来~

至少点个赞再走吧~

觉得还不错？可以在公众号菜单栏找到“赞赏”入口~