罗宾·米尔纳

罗宾·米尔纳（Robin Milner，1934—2010）是英国计算机科学家，全名Arthur John Robin Gorell Milner。他的研究横跨交互式定理证明、程序设计语言与并发系统，1991年获得图灵奖。1973至1994年间，他在爱丁堡大学工作，后来于1995年转赴剑桥大学。

米尔纳并不把这些领域视作互不相关的工具清单：程序如何表达、类型能排除哪些错误、多个进程怎样交互，都需要精确的数学说明。其工作同时依托合作环境，包括爱丁堡的基础研究团队，以及参与证明系统和语言设计的研究者。

参考：[1] [2]

LCF最初围绕达纳·斯科特提出的可计算函数逻辑展开，目标是让计算机辅助构造和检查证明，而不是宣称机器能自动证明所有程序正确。米尔纳在斯坦福开展相关工作后，继续在爱丁堡与迈克·戈登、克里斯·沃兹沃思等人发展系统。

ML中的名称意为元语言，早期用于描述LCF中的证明活动。把证明策略写成程序，需要兼顾表达能力与检查机制，类型系统因而成为语言设计的重要组成。早期ML后来发展出更广泛的用途，但不能把它与后来的Standard ML语言及其协作制定的正式定义混作同一时间完成的单人成果。

参考：[1] [2] [3]

1978年的类型多态论文说明，程序可以具有一般化的类型，同时由算法在编译阶段推导类型约束。例如，对列表逐项应用函数的map，既能处理整数，也能处理其他元素；其关键关系是输入函数从类型a映射到类型b，输入列表装有a，结果列表装有b。

算法W通过组合表达式的约束并进行合一，寻找相容类型。多态在这里不是任意混用值，而是同一计算结构遵守一致的类型关系。论文承认欣德利关于主类型的先行研究，并借助合一方法，不能把整个Hindley–Milner传统归为一人独创。类型可靠性针对特定语义中的类型错误，也不等于排除了所有逻辑错误。

参考：[3]

米尔纳对并发的研究包括CCS；他与约阿希姆·帕罗、戴维·沃克共同发表的1992年论文进一步阐述π演算。进程不仅能沿通道发送普通数据，也能传递通道名称，使接收方获得新的通信连接。

例如，进程P把原来供自己与R通信的通道名交给Q，Q便能沿该通道直接与R交互。这里的“移动”主要指通信拓扑变化，并非必须有设备在地理空间中移动。相较于只列出并行运行的程序，进程演算提供了讨论交互与行为等价的形式语言；相关模型的提出和发展同样应保留合作者与先行工作的边界。

参考：[2] [4]