Michael J. C. Gordon

From Wikipedia, the free encyclopedia

Michael J. C. Gordon

Born February 28, 1948 (1948-02-28) (age 60)
Ripon, Yorkshire, England
Residence Cambridgeshire
Citizenship United Kingdom
Nationality British
Fields Computer Science
Institutions University of Cambridge
Alma mater University of Edinburgh
Known for HOL theorem prover

Michael J. C. 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 1988, initially as a Reader, and from 1996 as a Professor. He was elected a Fellow of the Royal Society in 1994.

[edit] External links



Persondata
NAME Gordon, Michael J. C.
ALTERNATIVE NAMES
SHORT DESCRIPTION British computer scientist
DATE OF BIRTH February 28, 1948
PLACE OF BIRTH Ripon, Yorkshire, England
DATE OF DEATH
PLACE OF DEATH
This article about a British scientist is a stub. You can help Wikipedia by expanding it.
 This biographical article relating to a computer scientist is a stub. You can help Wikipedia by expanding it.