Michael John Caldwell Gordon FRS (28 de febrero de 1948 - 22 de agosto de 2017) fue un destacado científico 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 , Universidad de Cambridge , pero se transfirió a matemáticas . Durante sus estudios, en 1969 trabajó en el Laboratorio Nacional de Física de Londres durante el verano, obteniendo su primera exposición a las computadoras.
Gordon estudió su doctorado en la Universidad de Edimburgo , bajo la supervisión de Rod Burstall , y finalizó 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 emprendieron investigaciones juntos. [4]
Gordon dirigió el desarrollo del probador 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.