Michael J. C. Gordon
| Michael J. C. Gordon | |
|---|---|
 | |
| Born |
28 February 1948 Ripon, Yorkshire, England |
| Residence | Cambridgeshire |
| Citizenship | United Kingdom |
| Nationality | British |
| Fields | Computer Science |
| Institutions | University of Cambridge |
| Alma mater | University of Edinburgh |
| Thesis | Evaluation and denotation of pure LISP programs: a worked example in semantics (1973) |
| Known for | HOL theorem prover |
Michael John Caldwell "Mike" Gordon FRS (born 28 February 1948) is a British computer scientist.
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.[1] The first three were informal users' meetings with no published proceedings. The tradition now is for an annual conference in a continent different from 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.[2]
References
- ↑ "TPHOLS, conferences associated with theorem proving in higher-order logics". UK: University of Cambridge. Retrieved 28 January 2014.
- ↑ "Tools and Techniques for Verification of System Infrastructure". Retrieved 28 January 2014.
External links
- Mike Gordon home page
- Michael J. C. Gordon's publications indexed by the DBLP Bibliography Server at the University of Trier
|