Michael John Caldwell Gordon FRS (28 de febrero de 1948 - 22 de agosto de 2017) fue un informático británico . [2] [3]
Mike Gordon nació en Ripon , Yorkshire , Inglaterra . [4] Asistió a la escuela Dartington Hall y a la escuela Bedales . En 1966, fue aceptado para estudiar ingeniería en Gonville and Caius College de la Universidad de Cambridge , pero fue transferido 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 terminó en 1973 con una tesis titulada Evaluación y Denotación de Programas LISP Puros . Fue invitado a la Universidad de Stanford en California por John McCarthy , el inventor de LISP , para trabajar allí en su Laboratorio de Inteligencia Artificial . Gordon trabajó en el Laboratorio de Computación de la Universidad de Cambridge desde 1981, inicialmente como profesor, ascendido a lector 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, 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 dirigió el desarrollo del demostrador del teorema HOL . El sistema HOL es un entorno para la demostración interactiva de teoremas en una 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.
Ha habido una serie de conferencias internacionales sobre el sistema HOL, TPHOLs. [9] Las tres primeras fueron reuniones informales de usuarios sin actas publicadas. La tradición ahora es celebrar una conferencia anual en un continente diferente al lugar de la reunión anterior. A partir de 1996, el alcance se amplió para cubrir toda la demostración de teoremas en lógica de orden superior.
{{cite journal}}: Citar diario requiere |journal=( ayuda )