Michael J. C. Gordon
Template:Short description Template:Use dmy dates Template:Use British English Script error: No such module "Template wrapper".Template:Main otherScript error: No such module "Check for clobbered parameters".
Michael John Caldwell Gordon Template:Post-nominals (28 February 1948 – 22 August 2017) was a British computer scientist.[1][2]
Life
Mike Gordon was born in Ripon, Yorkshire, England.[3] He attended Dartington Hall School and Bedales School. In 1966, he was accepted to study engineering at Gonville and Caius College, University of Cambridge, but transferred to mathematics. During his studies, in 1969 he worked at the National Physical Laboratory in London during the summer, gaining his first exposure to computers.
Gordon studied for his PhD degree attthe University of Edinburgh, supervised by Rod Burstall, finishing in 1973 with a thesis entitled Evaluation and Denotation of Pure LISP Programs. He was invited to Stanford University in California by John McCarthy, the inventor of LISP, to work in his Artificial Intelligence Laboratory there. Gordon worked at the Cambridge University Computer Laboratory from 1981, initially as a lecturer, promoted to Reader in 1988 and Professor in 1996.
He was elected a Fellow of the Royal Society in 1994,[4] and in 2008 a two-day research meeting on Tools and Techniques for Verification of System Infrastructure was held there in honour of his 60th birthday.[5]
Mike Gordon was married to Avra Cohn, a PhD student of Robin Milner at the University of Edinburgh, and they undertook research together.[3]
He died in Cambridge after a brief illness and is survived by his wife and two sons.[1][6][7]
Work
Gordon led the development of the HOL theorem prover. The HOL system is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML. The system has a wide variety of uses, from formalising pure mathematics to the verification of industrial hardware.
There has been a series of international conferences on the HOL system, TPHOLs.[8] The first three were informal users' meetings with no published proceedings. The tradition now is for an annual conference on a different continent from the location of the previous meeting. From 1996, the scope broadened to cover all theorem proving in higher-order logics.
References
External links
Template:FRS 1994 Template:Authority control
- ↑ a b Script error: No such module "citation/CS1".
- ↑ Script error: No such module "Citation/CS1".
- ↑ a b Script error: No such module "Citation/CS1".
- ↑ Paulson, Lawrence C (2018). "Michael John Caldwell Gordon. 28 February 1948 – 22 August 2017". Biographical Memoirs of Fellows of the Royal Society. doi.org/10.1098/rsbm.2018.0019.
- ↑ Script error: No such module "citation/CS1".
- ↑ Script error: No such module "citation/CS1".
- ↑ Script error: No such module "Citation/CS1".
- ↑ Script error: No such module "citation/CS1".
- Pages with script errors
- 1948 births
- 2017 deaths
- People from Ripon
- People educated at Bedales School
- Alumni of Gonville and Caius College, Cambridge
- Alumni of the University of Edinburgh
- English computer scientists
- Formal methods people
- Members of the University of Cambridge Computer Laboratory
- Fellows of the Royal Society
- Scientists of the National Physical Laboratory (United Kingdom)