Michael J. C. Gordon
Encyclopedia
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.
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
(born February 28, 1948).
Mike Gordon led the development of the HOL theorem prover
HOL theorem prover
HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....
. 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
Ripon
Ripon is a cathedral city, market town and successor parish in the Borough of Harrogate, North Yorkshire, England, located at the confluence of two streams of the River Ure in the form of the Laver and Skell. The city is noted for its main feature the Ripon Cathedral which is architecturally...
, Yorkshire
Yorkshire
Yorkshire is a historic county of northern England and the largest in the United Kingdom. Because of its great size in comparison to other English counties, functions have been increasingly undertaken over time by its subdivisions, which have also been subject to periodic reform...
, England
England
England is a country that is part of the United Kingdom. It shares land borders with Scotland to the north and Wales to the west; the Irish Sea is to the north west, the Celtic Sea to the south west, with the North Sea to the east and the English Channel to the south separating it from continental...
. He gained his Ph.D.
Ph.D.
A Ph.D. is a Doctor of Philosophy, an academic degree.Ph.D. may also refer to:* Ph.D. , a 1980s British group*Piled Higher and Deeper, a web comic strip*PhD: Phantasy Degree, a Korean comic series* PhD Docbook renderer, an XML renderer...
at University of Edinburgh
University of Edinburgh
The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
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
Professor
A professor is a scholarly teacher; the precise meaning of the term varies by country. Literally, professor derives from Latin as a "person who professes" being usually an expert in arts or sciences; a teacher of high rank...
in 1996. He was elected a Fellow of the Royal Society
Royal Society
The Royal Society of London for Improving Natural Knowledge, known simply as the Royal Society, is a learned society for science, and is possibly the oldest such society in existence. Founded in November 1660, it was granted a Royal Charter by King Charles II as the "Royal Society of London"...
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.