Michael J. C. Gordon

Source: Wikipedia, the free encyclopedia.

Michael J. C. Gordon
Computer Science
InstitutionsStanford University
University of Cambridge
ThesisEvaluation and denotation of pure LISP programs: a worked example in semantics (1973)
Doctoral advisorRod Burstall[1]

Michael John Caldwell Gordon FRS (28 February 1948 – 22 August 2017) was a British computer scientist.[2][3]

Life

Mike Gordon was born in

Dartington Hall School and Bedales School. In 1966, he was accepted to study engineering at Gonville and Caius College, University of Cambridge, but transferred to mathematics. During his studies, in 1969 he worked at the National Physical Laboratory in London
during the summer, gaining his first exposure to computers.

Gordon studied for his

Cambridge University Computer Laboratory from 1981, initially as a lecturer, promoted to Reader in 1988 and Professor
in 1996.

He was elected a Fellow of the Royal Society in 1994,[5] 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.[6]

Mike Gordon was married to Avra Cohn, a PhD student of Robin Milner at the University of Edinburgh, and they undertook research together.[4]

He died in Cambridge after a brief illness and is survived by his wife and two sons.[2][7][8]

Work

Gordon led the development of the

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 formalising pure mathematics to verification of industrial hardware.

There has been a series of international conferences on the HOL system, TPHOLs.[9] 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

  1. ^ Michael J. C. Gordon at the Mathematics Genealogy Project
  2. ^
    Computer Laboratory, University of Cambridge
    . 2017. Retrieved 2 September 2017.
  3. .
  4. ^
    S2CID 47017843. {{cite journal}}: Cite journal requires |journal= (help
    )
  5. ^ Paulson, Lawrence C (2018). "Michael John Caldwell Gordon. 28 February 1948—22 August 2017". Biographical Memoirs of Fellows of the Royal Society. doi.org/10.1098/rsbm.2018.0019.
  6. ^ "Tools and Techniques for Verification of System Infrastructure". Retrieved 14 January 2023.
  7. ^ Kalvala, Sara (22 August 2017). "Sad news regarding Mike Gordon". HOL theorem-proving system. SourceForge. Retrieved 2 September 2017.
  8. .
  9. ^ "TPHOLS, conferences associated with theorem proving in higher-order logics". UK: University of Cambridge. Archived from the original on 7 May 2008. Retrieved 28 January 2014.

External links