Robin Milner 1934-2010

摘要

A special session of the symposium pays tribute to Robin Milner; the session features talks by Robert Harper (Carnegie Mellon University), John Harrison (Intel), and Alan Jeffrey (Bell Labs), and is organised by Andrew D. Gordon (Microsoft Research) and Peter Sewell (University of Cambridge). Robin Milner was born near Plymouth in England. He was educated at Eton College, Windsor, and went up to King's College, Cambridge, in 1954. In between, his national service was with the Royal Engineers, in Egypt. After university he was first a school teacher and then worked in London as a programmer at Ferranti, an early British computer company. In 1963 he took a job as lecturer at City University, and started research on the side-he never studied for a PhD. In 1968, he moved to Swansea to become a research assistant. He was excited by Scott's lectures in 1969 in Oxford on domain theory. During this time he learnt about Floyd's work on verification, and got to know Tony Hoare, and started trying to verify programs. After meeting Zohar Manna during a visit to Carnegie Mellon University, he got a job with John McCarthy at Stanford in 1971. There he built the theorem proving system Stanford LCF, which he would later substantially refine with the addition of a metalanguage (ML) for constructing proofs.