阿瑟·约翰·罗宾·戈雷尔·米尔纳(1934年1月13日-2010年3月20日)是英国计算机科学家,1991年ACM图灵奖得主。他因三项主要贡献而广受认可:开发可计算函数逻辑(LCF)和ML编程语言、通信系统演算(CCS)以及π演算。他的工作为自动定理证明、类型系统以及并发和移动系统的理论分析奠定了坚实基础。
米尔纳的研究弥合了理论计算机科学与实用语言设计之间的鸿沟,影响了从函数式编程到分布式计算等多个领域。他后期关于大图(bigraphs)的研究旨在统一并发和普适计算的模型,尽管这项工作在他去世时尚未完成。
生平、教育与职业生涯
米尔纳出生于英格兰普利茅斯附近的耶尔普顿,成长于军人家庭。1947年,他获得伊顿公学的国王奖学金,并于1952年获得伊顿公学最高数学奖汤姆林奖。在皇家工兵部队担任少尉后,他进入剑桥大学国王学院,于1957年毕业。
他的早期职业生涯包括担任学校教师,随后在费兰蒂公司担任程序员。他进入学术界后,先后在伦敦城市大学、斯旺西大学和斯坦福大学任职。1973年,他加入爱丁堡大学,并共同创立了计算机科学基础实验室(LFCS)。1995年,他返回剑桥大学担任计算机实验室主任,后虽卸任该职务,但仍在此活跃。从2009年起,他担任苏格兰信息学与计算机科学联盟高级研究员,并在爱丁堡大学兼任计算机科学教席。
米尔纳于2010年3月20日在剑桥因心脏病发作去世。他的妻子露西在他去世前不久离世。
对编程语言的贡献
米尔纳在LCF(最早的自动定理证明工具之一)上的工作促成了ML的诞生。该语言引入了使用算法W的多态类型推断和类型安全的异常处理。ML是第一种具有自动推断类型系统的语言,这一特性对Haskell和OCaml等语言产生了深远影响。米尔纳还因重新发现Hindley–Milner类型系统而受到赞誉,该系统是多态类型的基础。
他在并发方面的理论框架包括20世纪70年代末开发的通信系统演算(CCS)及其后继者π演算(于20世纪90年代初提出)。CCS将进程建模为交互代理,而π演算则扩展了这一模型,允许移动通信信道。这些形式化方法成为并发和分布式系统研究的基石。
在去世时,米尔纳正在研究大图,这是一种旨在涵盖CCS和π演算以支持普适计算的形式化方法。这项工作旨在建模交互代理的空间和时间方面。
荣誉与奖项
米尔纳获得了众多荣誉。1988年,他成为皇家学会会士和英国计算机学会杰出会士。1991年,他获得ACM图灵奖。1994年,他当选为ACM会士。2004年,爱丁堡皇家学会授予他皇家奖章,以表彰他为全球公众带来的福祉。2008年,他因在LCF、ML、CCS和π演算方面的基础性贡献,当选为美国国家工程院外籍院士。
有两个奖项以他的名字命名:皇家学会米尔纳奖和ACM SIGPLAN罗宾·米尔纳青年研究者奖。
主要出版物
米尔纳撰写了几本有影响力的著作。他1980年的专著《通信系统演算》介绍了CCS。《通信与并发》(1989年)扩展了这一工作。他与马德斯·托夫特和罗伯特·哈珀合著了《标准ML定义》(1990年),并于1997年与大卫·麦昆合作出版了修订版。《通信与移动系统:π演算》(1999年)详细阐述了π演算。他的最后一部著作《通信代理的空间与运动》(2009年)展示了他对大图的研究。
遗产
米尔纳的影响遍及计算机科学的多个领域,从类型理论到并发。他的思想塑造了现代函数式编程和系统的形式化验证。人工智能社区,特别是在机器学习和神经网络等领域,依赖于可追溯至ML血统的编程语言和工具。他在并发方面的工作与分布式系统和云计算仍然相关,正如亚马逊网络服务和谷歌云等平台所示。
他的遗产通过麻省理工学院计算机科学与人工智能实验室和斯坦福人工智能实验室等机构得以延续,这些机构继续推进他所帮助建立的领域。皇家学会和ACM通过奖项纪念他,以表彰在编程语言和并发领域做出贡献的青年研究者。