Robin Milner

简介

Robin Milner（罗宾·米尔纳，1934-2010），英国计算机科学家，1991 年图灵奖得主，长期任职于爱丁堡大学与剑桥大学。

主要贡献

Milner 的三大贡献均具奠基意义。其一，交互式定理证明器 LCF 确立了「用可编程策略构造证明、以小内核保证正确性」的架构，至今仍是证明助手的标准范式。其二，为 LCF 设计的元语言 ML 发展为独立编程语言，其多态类型推断（与 Damas 形式化的 Algorithm W）成为静态类型函数式语言的基石，直接孕育了 Standard ML、OCaml、Haskell 一系。其三，他创立了并发理论中的 CCS（通信系统演算），后又与合作者提出 π 演算，为移动并发进程提供了数学模型。

影响

「良类型程序不会出错」（well-typed programs cannot go wrong）这一名言即出自 Milner，概括了类型安全的语义学内涵。