Education
University of Edinburgh.
University of Edinburgh.
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 Master of Laws. 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 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 Doctor of Philosophy 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.
Royal Society.
