| Nacimiento |
18 de abril de 1962 Montreal |
|---|---|
| Nacionalidad | canadiense |
| Actividad | Informático |
| Trabajé para | Investigación de Microsoft |
|---|---|
| Áreas | Ciencias de la computación , lógica matemática |
| Sitio web | www.msr-inria.fr/researchers/georges-gonthier |
Georges Gonthier es un investigador canadiense en informática que lleva a cabo sus investigaciones en Gran Bretaña y Francia . Sus áreas de interés son el diseño de lenguajes de programación y su semántica, la teoría de la competencia en programación y su aplicación a la seguridad, métodos y herramientas para la verificación formal de programas informáticos y teorías matemáticas. Es notablemente conocido por el desarrollo completo, verificado mecánicamente por computadora, de la demostración del teorema de los cuatro colores .
Georges Gonthier entre otros trabajó en competidores y lenguajes sincrónicos, en particular el lenguaje Esterel de Gérard Berry , en la reducción del cálculo lambda con Martín Abadi y Jean-Jacques Levy , y en comunicaciones de seguridad de procesos distribuidas con Abadi y Cedric Fournet .
Su investigación actual se centra en el uso de asistentes de prueba basados en la teoría de tipos , diseñados y utilizados por lógicos e informáticos, en áreas más amplias de las matemáticas. En 2005, su verificación automática de la demostración del teorema de los cuatro colores totalmente formalizada en el sistema Coq puso fin a las dudas de la comunidad matemática sobre la validez de las demostraciones automatizadas de este resultado. Desde el grupo de Componentes Matemáticos, dirige el centro común Microsoft - INRIA , que trabaja en la formalización de matemáticas más fundamentales, incluida la teoría de grupos finitos .
Georges Gonthier recibió el Gran Premio “Ciencias de la Computación” de la Fundación Corporativa EADS en 2011 .
La 20 de septiembre de 2012, anunció que había completado la formalización en Coq de la demostración del teorema de Feit-Thompson , luego de 6 años de trabajo con su equipo. Este resultado confirma la exactitud de la prueba de 250 páginas escrita en 1963.