Michael J. C. Gordon facts for kids
Quick facts for kids
Michael J. C. Gordon
|
|
---|---|
![]() |
|
Born | |
Died | 22 August 2017 Cambridge, England
|
(aged 69)
Alma mater | Gonville and Caius College, Cambridge University of Edinburgh |
Known for | HOL theorem prover |
Scientific career | |
Fields | Computer Science |
Institutions | Stanford University University of Cambridge |
Thesis | Evaluation and denotation of pure LISP programs: a worked example in semantics (1973) |
Doctoral advisor | Rod Burstall |
Michael John Caldwell Gordon (born February 28, 1948 – died August 22, 2017) was a very important British computer scientist. He was known for his work in making sure computer systems work correctly and safely. He was also a Fellow of the Royal Society, which is a big honor for scientists in the UK.
Contents
About His Life
Mike Gordon was born in Ripon, a town in Yorkshire, England. He went to two schools called Dartington Hall School and Bedales School. In 1966, he started studying engineering at Gonville and Caius College at the University of Cambridge. But he soon changed his mind and decided to study mathematics instead.
In 1969, while still a student, he worked at the National Physical Laboratory in London. This was his first time working with computers, and it sparked his interest in them!
His Studies and Career
Mike Gordon then went on to get his PhD degree at the University of Edinburgh. He finished his PhD in 1973. His research was about how computer programs work.
After his PhD, he was invited to Stanford University in California. He worked there with John McCarthy, who was famous for inventing a computer language called LISP.
In 1981, Gordon returned to the UK and started working at the Cambridge University Computer Laboratory. He began as a lecturer, teaching students about computer science. Over the years, he became a Reader in 1988 and then a full Professor in 1996. This shows how dedicated and skilled he was in his field.
In 1994, he was chosen to be a Fellow of the Royal Society. This is a very special award given to top scientists. In 2008, a special meeting was held to celebrate his 60th birthday and his amazing contributions to computer science.
Mike Gordon was married to Avra Cohn, who was also a computer scientist. They even worked on research projects together! He passed away in Cambridge in 2017, leaving behind his wife and two sons.
His Important Work
Mike Gordon is most famous for leading the creation of something called the HOL theorem prover. This is a special computer system that helps people prove if computer programs or hardware designs are correct.
What is a Theorem Prover?
Imagine you have a very complicated puzzle or a set of rules. A theorem prover is like a super-smart assistant that can check if something follows all those rules perfectly. In computer science, this is super important for making sure that things like computer chips or software for airplanes work exactly as they should, without any mistakes.
The HOL system is special because it uses something called "higher-order logic." This is a very advanced way of thinking about rules and proofs. It also uses a programming language called ML, which makes it very flexible and powerful. People have used the HOL system for many different things, from proving ideas in pure mathematics to checking if industrial computer parts are safe and reliable.
Conferences and Community
Because the HOL system was so important, there have been many international conferences about it. These meetings, called TPHOLs, bring together experts from all over the world. They share new ideas and discuss how to make computer systems even more trustworthy. These conferences started as small user meetings and grew into big annual events, showing how much impact Mike Gordon's work had on the field of computer science.