- Michael J. C. Gordon
-
Michael J. C. Gordon
Born February 28, 1948
Ripon, Yorkshire, EnglandResidence Cambridgeshire Citizenship United Kingdom Nationality British Fields Computer Science Institutions University of Cambridge Alma mater University of Edinburgh Known for HOL theorem prover Michael John Caldwell Gordon, British computer scientist (born February 28, 1948).
Mike 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 formalizing pure mathematics to verification of industrial hardware.
There has been a series of international conferences on the HOL system, TPHOLs. The first three were informal users' meetings with no published proceedings. The tradition now is for an annual conference in a continent different to the location of the previous meeting. From 1996 the scope broadened to cover all theorem proving in higher-order logics.
Gordon was born in Ripon, Yorkshire, England. He gained his Ph.D. at University of Edinburgh in 1973 with a thesis entitled Evaluation and Denotation of Pure LISP Programs. He has worked at the Cambridge University Computer Laboratory since 1981, initially as a Lecturer and moving to Reader in 1988 and Professor in 1996. He was elected a Fellow of the Royal Society in 1994, 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.
External links
- Home page
- Michael J. C. Gordon bibliography in the DBLP database
- TPHOLS, conferences associated with theorem proving in higher-order logics
- Tools and Techniques for Verification of System Infrastructure
Categories:- 1948 births
- Living people
- People from Ripon
- British computer scientists
- Fellows of the Royal Society
- Alumni of Gonville and Caius College, Cambridge
- Alumni of the University of Edinburgh
- Formal methods people
- Members of the University of Cambridge Computer Laboratory
- British scientist stubs
- Computer scientist stubs
Wikimedia Foundation. 2010.