Robin Milner was a British computer scientist whose work shaped both the theory of programming languages and the practical tools built on that theory. In 1991 he received the A.M. Turing Award, described by his home institution as the highest honour in computer science.
The Turing citation recognized three lines of work. The first was LCF, “the mechanisation of Scott’s Logic of Computable Functions,” noted as probably the first theoretically based yet practical tool for machine-assisted proof construction. The second was ML, “the first language to contain polymorphic type inference together with a type-safe exception handling mechanism.” The third was CCS, a general theory of concurrency.
ML grew out of the LCF project: it began as the “metalanguage” used to write proof tactics for the LCF prover, and its type system had to guarantee that those tactics could not be misused. From that practical need Milner developed a polymorphic type discipline and a compile-time type-checking algorithm, which he set out in his 1978 paper “A Theory of Type Polymorphism in Programming.” The citation calls the type-inference algorithm applied to a full language a major theoretical advance.
Milner’s later work turned to concurrency, where he built two frameworks for analyzing communicating systems: the Calculus of Communicating Systems (CCS) and its successor, the pi-calculus. His career is often cited as a model of how mathematical theory and engineering practice can feed back into one another.