Michael John Caldwell Gordon FRS (28 de febrero de 1948 - 22 de agosto de 2017) fue un científico informático británico . [2] [3]
Mike Gordon nació en Ripon , Yorkshire , Inglaterra . [4] Asistió a la Dartington Hall School y a la Bedales School . En 1966, fue aceptado para estudiar ingeniería en el Gonville and Caius College , de la Universidad de Cambridge , pero se trasladó a matemáticas . Durante sus estudios, en 1969 trabajó en el Laboratorio Nacional de Física de Londres durante el verano, obteniendo su primer contacto con las computadoras.
Gordon estudió su doctorado en la Universidad de Edimburgo , supervisado por Rod Burstall , y finalizó en 1973 con una tesis titulada Evaluation and Denotation of Pure LISP Programs . Fue invitado a la Universidad de Stanford en California por John McCarthy , el inventor de LISP , para trabajar en su Laboratorio de Inteligencia Artificial allí. Gordon trabajó en el Laboratorio de Computación de la Universidad de Cambridge desde 1981, inicialmente como profesor, ascendido a Reader en 1988 y profesor en 1996.
Fue elegido miembro de la Royal Society en 1994, [5] y en 2008 se celebró allí una reunión de investigación de dos días sobre herramientas y técnicas para la verificación de la infraestructura del sistema en honor a su 60º cumpleaños. [6]
Mike Gordon estaba casado con Avra Cohn, una estudiante de doctorado de Robin Milner en la Universidad de Edimburgo , y realizaron investigaciones juntos. [4]
Murió en Cambridge después de una breve enfermedad y le sobreviven su esposa y dos hijos. [2] [7] [8]
Gordon lideró el desarrollo del demostrador de teoremas HOL . El sistema HOL es un entorno para la demostración interactiva de teoremas en lógica de orden superior . Su característica más destacada es su alto grado de programabilidad a través del metalenguaje ML . El sistema tiene una amplia variedad de usos, desde la formalización de matemáticas puras hasta la verificación de hardware industrial.
Se han celebrado una serie de conferencias internacionales sobre el sistema HOL, las TPHOL [9] . Las tres primeras fueron reuniones informales de usuarios sin actas publicadas. Ahora la tradición es que se celebre una conferencia anual en un continente diferente de la ubicación de la reunión anterior. A partir de 1996, el alcance se amplió para cubrir todas las demostraciones de teoremas en lógica de orden superior.
{{cite journal}}: Requiere citar revista |journal=( ayuda )