Robin Milner

Milner created ML (Meta Language) in the early 1970s at the University of Edinburgh as the metalanguage for his LCF theorem prover. ML pioneered polymorphic type inference and type-safe exception handling, and its descendants include Standard ML, OCaml, and F#, while its ideas influenced Haskell and many other modern languages.

Milner developed the π-calculus in the early 1990s as a formal model for concurrent systems whose communication topology can change dynamically, such as mobile agent networks. Unlike earlier process calculi, the π-calculus allows communication channels themselves to be transmitted as messages, making it suitable for modeling modern distributed systems.

Milner developed LCF (Logic for Computable Functions) starting in 1972 at Stanford and later at Edinburgh, creating it to prove properties about programs in a rigorous, machine-checked manner. The system introduced the concept of programmable proof strategies called 'tactics,' which became fundamental to later proof assistants like Coq and Isabelle.

Milner received the 1991 Turing Award for three major contributions: the ML programming language, the LCF theorem prover, and CCS (Calculus of Communicating Systems), a 1980 process algebra for modeling concurrent computation. Together these works established him as a foundational figure in both programming language theory and concurrency research.