Milner is generally regarded as having made three major contributions to computer science. He developed LCF, one of the first tools forautomated theorem proving. The language he developed for LCF, ML, was the first language with polymorphic type inference and type-safeexception handling. In a very different area, Milner also developed a theoretical framework for analyzing concurrent systems, the calculus of communicating systems (CCS), and its successor, the pi-calculus. At the time of his death, he was working on bigraphs, a formalism for ubiquitous computing subsuming CCS and the pi-calculus.