罗宾·米尔纳（Robin Milner，1934年1月13日 - 2010年3月20日），英国计算机科学家，致力于数学计算理论的研究，因其在自动定理证明器、机器学习及计算机编程语言以及并发一般理论方面的工作，荣获1991年图灵奖。

米尔纳1934年1月13日出生于英国普利茅斯耶尔姆普顿的一个军人家庭，父亲是英国陆军上校。

米尔纳就读于伊顿公学，1952年获得奖学金进入剑桥大学。随后参加服役不得不延迟两年入学，在苏伊士运河英国陆军皇家工兵部队参军两年。 1954年服役结束后进入剑桥大学，1957年获得剑桥大学数学学士学位。

1956年，米尔纳第一次接触计算机，他参加了一门为期10天的短期编程课程，学习莫里斯·威尔克斯的 EDSAC 计算机。起初米尔纳对计算机并不感兴趣，他甚至认为编写代码不够优雅。但是他对工具帮助人类扩大影响力非常感兴趣，例如汽车让人的活动范围大大增加，外骨骼让身体不是很强壮的人也可以攀登高峰。在他那个年代，他在家中杂物间整齐摆放了各种凿子、钉子、锥子。随着计算机的进步，米尔纳开始对计算机作为工具产生了浓厚的兴趣，他意识到计算机不仅仅是计算工具，更有可能成为「心灵的工具」。

米尔纳从事过多种工作，1959年至1960年间在玛丽勒本发文学校教授数学，后来成为费兰蒂有限公司程序员开发编译器。1963年，米尔纳离开费兰蒂，前往伦敦城市大学任教，教授工程专业数学，并开始研究人工智能及其在数据库中的应用。

1968年，米尔纳接受了威尔士大学斯旺分享的研究职位，专注于程序验证、自动定理证明和语义学，这段时间他开始发表关于「程序方案」的论文，这是一种早期的流程图式操作模型。米尔纳经常前往牛津听 Christopher Strachey 和 Dana Scott 的讲座，受他们启发米尔纳开始对程序验证和语义学产生兴趣，他后来表示这是他研究生涯的真正起点。

1971年，米尔纳受邀前往美国斯坦福大学，在斯坦福大学人工智能实验室，作为约翰·麦卡锡人工智能项目的研究助理工作了两年。米尔纳更关心人类智能如何被「放大」，而不是人工智能独立可能实现什么。

LCF（Logic for Computable Functions）是米尔纳提出的形式化逻辑系统的一个数学模型，最早的自动定理证明工具之一。LCF 不仅可以有效建模，还可以方便地验证计算机程序的正确性，受到学术界的高度评价。在斯坦福大学人工智能实验室工作期间，曾用 LCF 证明了一个很复杂的编译器的正确性，受到麦卡锡的高度赞扬。

1973年，米尔纳接受爱丁堡大学职位回到英国，协助设计了机器学习元语言，这是一种为实现自动定理求解而开发的计算机编程语言。

1990年，米尔纳出版了《通信系统演算》专著。1995年，米尔纳回到剑桥，担任学校计算机实验室负责人。1998年，米尔纳出版了新书《通信与并发》。

人类设计的每一个工具都是义肢装置，每种义肢装置都有控制手段。许多工具是无力的，它们的控制是手动的。相比之下，计算机是有史以来最复杂的工具，它们是心灵的工具：控制手段绝非肌肉化——主要是语言的。简单来说，计算机的多样性正好等同于我们用来定义其行为的语言多样性，而这似乎是无边无际的。

米尔纳于2001年退休，但他并未停止研究，在2009年他出版了最后一本书《交流代理的空间与运动》

2010年3月20日，在他的妻子葬礼结束几天后，死于心脏病发作，在英国剑桥去世，享年76岁。

参考资料

1. https://baike.baidu.com/item/%E7%BD%97%E5%AE%BE%C2%B7%E7%B1%B3%E5%B0%94%E7%BA%B3/7868253?structureClickId=7868253&structureId=ced913fd22dfe016c93805da&structureItemId=8a0f553971607fe5f74f8734&lemmaFrom=starMapContent_star&fromModule=starMap_content&lemmaIdFrom=324645
2. https://www.britannica.com/biography/Robin-Milner
3. https://amturing.acm.org/award_winners/milner_1569367.cfm
4. https://blog.csdn.net/wt349711891/article/details/5435296