图灵奖:罗宾·米尔纳(1991)

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

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

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

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)及其继承者π演算

~~

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

至少点个赞再走吧~

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

图灵奖:罗宾·米尔纳(1991)

https://xlindo.com/kewenlu2023/posts/c9c3354d/

Author

xlindo

Posted on

2023-12-19

Updated on

2024-01-16

Licensed under

Comments