Editing Robin Milner (section)

==Contributions==

Milner is generally regarded as having made three major contributions to [[computer science]]. He developed [[Logic for Computable Functions]] (LCF), one of the first tools for [[automated theorem proving]]. The language he developed for LCF, [[ML programming language|ML]], was the first language with [[polymorphism (computer science)|polymorphic]] [[type inference]], type-safe [[exception handling]], and an automatically inferred type system, using [[algorithm W]]. Milner also developed two theoretical frameworks for analyzing [[concurrent systems]], the [[calculus of communicating systems]] (CCS), and its successor, the [[pi-calculus|{{pi}}-calculus]].

At the time of his death, he was working on [[bigraphs]], a formalism for [[ubiquitous computing]] subsuming CCS and the {{pi}}-calculus.<ref name="bigraphs">{{cite web |url= http://www.cl.cam.ac.uk/~rm135/uam-theme.html|title=The Bigraphical Model |first=Robin |last=Milner |publisher=University of Cambridge |access-date=7 November 2009 |quote=Bigraphs [...] are proposed as a '''Ubiquitous Abstract Machine''', playing the foundational role for ubiquitous computing that the von Neumann machine has played for sequential computing. }}</ref> He is also credited for rediscovering the [[Hindley–Milner type system]].