Michael John Caldwell Gordon FRS (28 February 1948 – 22 August 2017) was a British

computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...

Life

Mike Gordon was born in

Ripon Ripon () is a cathedral city in the Borough of Harrogate, North Yorkshire, England. The city is located at the confluence of two tributaries of the River Ure, the Laver and Skell. Historically part of the West Riding of Yorkshire, the city ...

Yorkshire Yorkshire ( ; abbreviated Yorks), formally known as the County of York, is a Historic counties of England, historic county in northern England and by far the largest in the United Kingdom. Because of its large area in comparison with other Eng ...

England England is a country that is part of the United Kingdom. It shares land borders with Wales to its west and Scotland to its north. The Irish Sea lies northwest and the Celtic Sea to the southwest. It is separated from continental Europe b ...

. He attended

Dartington Hall School Dartington Hall in Dartington, near Totnes, Devon, England, is an historic house and country estate of dating from medieval times. The group of late 14th century buildings are Grade I listed; described in Pevsner's Buildings of England as "on ...

and

Bedales School Bedales School is a co-educational, boarding and day independent school in the village of Steep, near the market town of Petersfield in Hampshire, England. It was founded in 1893 by John Haden Badley in reaction to the limitations of conventio ...

. In 1966, he was accepted to study

engineering Engineering is the use of scientific method, scientific principles to design and build machines, structures, and other items, including bridges, tunnels, roads, vehicles, and buildings. The discipline of engineering encompasses a broad rang ...

Gonville and Caius College Gonville and Caius College, often referred to simply as Caius ( ), is a constituent college of the University of Cambridge in Cambridge, England. Founded in 1348, it is the fourth-oldest of the University of Cambridge's 31 colleges and one of th ...

University of Cambridge , mottoeng = Literal: From here, light and sacred draughts. Non literal: From this place, we gain enlightenment and precious knowledge. , established = , other_name = The Chancellor, Masters and Schola ...

, but transferred to

mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...

. During his studies, in 1969 he worked at the National Physical Laboratory in

London London is the capital and largest city of England and the United Kingdom, with a population of just under 9 million. It stands on the River Thames in south-east England at the head of a estuary down to the North Sea, and has been a majo ...

during the summer, gaining his first exposure to computers. Gordon studied for his

PhD degree A Doctor of Philosophy (PhD, Ph.D., or DPhil; Latin: or ') is the most common degree at the highest academic level awarded following a course of study. PhDs are awarded for programs across the whole breadth of academic fields. Because it is a ...

University of Edinburgh The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 15 ...

, supervised by

Rod Burstall Rodney Martineau "Rod" Burstall FRSE (born 1934) is a British computer scientist and one of four founders of the Laboratory for Foundations of Computer Science at the University of Edinburgh. Biography Burstall studied physics at the Universi ...

, finishing in 1973 with a thesis entitled ''Evaluation and Denotation of Pure LISP Programs''. He was invited to

Stanford University Stanford University, officially Leland Stanford Junior University, is a private research university in Stanford, California. The campus occupies , among the largest in the United States, and enrolls over 17,000 students. Stanford is consider ...

California California is a U.S. state, state in the Western United States, located along the West Coast of the United States, Pacific Coast. With nearly 39.2million residents across a total area of approximately , it is the List of states and territori ...

by John McCarthy, the inventor of

LISP A lisp is a speech impairment in which a person misarticulates sibilants (, , , , , , , ). These misarticulations often result in unclear speech. Types * A frontal lisp occurs when the tongue is placed anterior to the target. Interdental lisping ...

, to work in his Artificial Intelligence Laboratory there. Gordon worked at the

Cambridge University Computer Laboratory The Department of Computer Science and Technology, formerly the Computer Laboratory, is the computer science department of the University of Cambridge. it employed 35 academic staff, 25 support staff, 35 affiliated research staff, and about 15 ...

from 1981, initially as a lecturer, promoted to

Reader A reader is a person who reads. It may also refer to: Computing and technology * Adobe Reader (now Adobe Acrobat), a PDF reader * Bible Reader for Palm, a discontinued PDA application * A card reader, for extracting data from various forms of ...

in 1988 and

Professor Professor (commonly abbreviated as Prof.) is an Academy, academic rank at university, universities and other post-secondary education and research institutions in most countries. Literally, ''professor'' derives from Latin as a "person who pr ...

in 1996. He was elected a

Fellow of the Royal Society Fellowship of the Royal Society (FRS, ForMemRS and HonFRS) is an award granted by the judges of the Royal Society of London to individuals who have made a "substantial contribution to the improvement of natural science, natural knowledge, incl ...

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. Mike Gordon was married to Avra Cohn, a PhD student of

Robin Milner Arthur John Robin Gorell Milner (13 January 1934 – 20 March 2010), known as Robin Milner or A. J. R. G. Milner, was a British computer scientist, and a Turing Award winner.

at the

, and they undertook research together. He died in Cambridge after a brief illness and is survived by his wife and two sons.

Work

Gordon led the development of the

HOL theorem prover HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defin ...

. The HOL system is an environment for interactive

theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

in a

higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...

. Its most outstanding feature is its high degree of programmability through the meta-language ML. The system has a wide variety of uses, from formalising 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.

References

External links

Mike Gordon home page
{{DEFAULTSORT:Gordon, Michael J. C. 1948 births 2017 deaths People from Ripon People educated at Bedales School Alumni of Gonville and Caius College, Cambridge Alumni of the University of Edinburgh English computer scientists Formal methods people Members of the University of Cambridge Computer Laboratory Fellows of the Royal Society