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

computer scientist A computer scientist is a scientist who specializes in the academic study of computer science. Computer scientists typically work on the theoretical side of computation. Although computer scientists can also focus their work and research on ...

Life

Mike Gordon was born in

Ripon Ripon () is a cathedral city and civil parish in North Yorkshire, England. The city is located at the confluence of two tributaries of the River Ure, the Laver and Skell. Within the boundaries of the historic West Riding of Yorkshire, the ...

Yorkshire Yorkshire ( ) is an area of Northern England which was History of Yorkshire, historically a county. Despite no longer being used for administration, Yorkshire retains a strong regional identity. The county was named after its county town, the ...

, England. 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 ...

and

Bedales School Bedales School is a coeducational boarding and day public school, in the village of Steep, near the market town of Petersfield in Hampshire, England. It was founded in 1893 by Amy Garrett Badley and John Haden Badley in reaction to the li ...

. In 1966, he was accepted to study

engineering Engineering is the practice of using natural science, mathematics, and the engineering design process to Problem solving#Engineering, solve problems within technology, increase efficiency and productivity, and improve Systems engineering, s ...

Gonville and Caius College Gonville and Caius College, commonly known as Caius ( ), is a constituent college of the University of Cambridge in Cambridge, England. Founded in 1348 by Edmund Gonville, it is the fourth-oldest of the University of Cambridge's 31 colleges an ...

University of Cambridge The University of Cambridge is a Public university, public collegiate university, collegiate research university in Cambridge, England. Founded in 1209, the University of Cambridge is the List of oldest universities in continuous operation, wo ...

, but transferred to

mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...

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

London London is the Capital city, capital and List of urban areas in the United Kingdom, largest city of both England and the United Kingdom, with a population of in . London metropolitan area, Its wider metropolitan area is the largest in Wester ...

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

PhD degree A Doctor of Philosophy (PhD, DPhil; or ) is a terminal degree that usually denotes the highest level of academic achievement in a given discipline and is awarded following a course of graduate study and original research. The name of the deg ...

attthe

University of Edinburgh The University of Edinburgh (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...

, supervised by

Rod Burstall Rodney Martineau Burstall (11 November 1934 – 13 February 2025) was a British computer scientist who was one of four founders of the Laboratory for Foundations of Computer Science at the University of Edinburgh. Biography Burstall studied p ...

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

Stanford University Leland Stanford Junior University, commonly referred to as Stanford University, is a Private university, private research university in Stanford, California, United States. It was founded in 1885 by railroad magnate Leland Stanford (the eighth ...

California California () is a U.S. state, state in the Western United States that lies on the West Coast of the United States, Pacific Coast. It borders Oregon to the north, Nevada and Arizona to the east, and shares Mexico–United States border, an ...

John McCarthy John McCarthy may refer to: Government * John George MacCarthy (1829–1892), Member of Parliament for Mallow constituency, 1874–1880 * John McCarthy (Irish politician) (1862–1893), Member of Parliament for the Mid Tipperary constituency, ...

, the inventor of

LISP Lisp (historically LISP, an abbreviation of "list processing") is a family of programming languages with a long history and a distinctive, fully parenthesized Polish notation#Explanation, prefix notation. Originally specified in the late 1950s, ...

, 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 56 faculty members, 45 support staff, 105 research staff, and about 205 researc ...

from 1981, initially as a lecturer, promoted to Reader in 1988 and

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

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 Fellows 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) was a British computer scientist, and a Turing Award winner.University of Edinburgh The University of Edinburgh (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...

, 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 Proof assistant, interactive theorem proving systems using similar Higher-order logic, (higher-order) logics and implementation strategies. Systems in this family follow the LCF (theorem prover), LCF ( ...

. 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 majo ...

in a

higher-order logic In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...

. 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 the 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 on a different continent 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 Scientists of the National Physical Laboratory (United Kingdom)