Michael John Caldwell Gordon, British computer scientist. 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 ML. 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.

PropertyValue
dbpedia-owl:Person/almaMater
dbpedia-owl:Person/birthDate
  • 1948-02-28 (xsd:date)
dbpedia-owl:Person/birthPlace
dbpedia-owl:Person/citizenship
dbpedia-owl:Person/knownFor
dbpedia-owl:Person/nationality
dbpedia-owl:Person/residence
dbpedia-owl:almaMater
dbpedia-owl:birthDate
  • 1948-02-28 (xsd:date)
dbpedia-owl:birthPlace
dbpedia-owl:citizenship
dbpedia-owl:knownFor
dbpedia-owl:nationality
dbpedia-owl:residence
dbpedia-owl:thumbnail
dbpprop:abstract
  • Michael John Caldwell Gordon, British computer scientist. 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 ML. 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 to 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 Ph.D. 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.
dbpprop:almaMater
dbpprop:birthDate
dbpprop:birthPlace
dbpprop:citizenship
dbpprop:field
dbpprop:hasPhotoCollection
dbpprop:id
  • g/Gordon:Michael_J=_C=
dbpprop:imageWidth
  • 200px
dbpprop:knownFor
dbpprop:name
  • Gordon, Michael J. C.
  • Michael J. C. Gordon
dbpprop:nationality
dbpprop:reference
dbpprop:residence
dbpprop:shortDescription
  • British computer scientist
dbpprop:wikiPageUsesTemplate
dbpprop:wordnet_type
dbpprop:workInstitution
rdf:type
rdfs:comment
  • Michael John Caldwell Gordon, British computer scientist. 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 ML. 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.
rdfs:label
  • Michael J. C. Gordon
owl:sameAs
skos:subject
foaf:depiction
foaf:givenname
  • Michael J. C.
  • Michael J. C.
foaf:name
  • Michael J. C. Gordon
  • Michael J. C. Gordon
foaf:page
foaf:surname
  • Gordon
  • Gordon
is dbpprop:redirect of
is owl:sameAs of