Gérard Huet


Gérard Pierre Huet ( francés:  [y.ɛ] ; nacido el 7 de julio de 1947) es un informático, lingüista y matemático francés. Es director senior de investigación en INRIA y es conocido sobre todo por sus importantes y fundamentales contribuciones a la teoría de tipos, la teoría del lenguaje de programación y la teoría de la computación .

Gérard Huet se graduó en la Université Denis Diderot (París VII), la Case Western Reserve University y la Université de Paris . [ cita requerida ]

Es director senior de investigación en INRIA , miembro de la Academia de Ciencias de Francia y miembro de la Academia Europaea . Anteriormente fue profesor invitado en el Instituto Asiático de Tecnología en Bangkok , profesor invitado en la Universidad Carnegie Mellon e investigador invitado en SRI International .

Es el autor de un algoritmo de unificación para cálculo lambda de tipo simple y de un método de prueba completo para la teoría de tipos de Church ( resolución restringida ). Trabajó en el editor del programa Mentor entre 1974 y 1977 con Gilles Kahn . Trabajó en el sistema de prueba ecuacional Knuth -Bendix (KB) en 1978-1984 con Jean-Marie Hullot . Dirigió el proyecto Formel en la década de 1980, que desarrolló el lenguaje de programación Caml . Diseñó el cálculo de construcciones en 1984 con Thierry Coquand . Dirigió el proyecto Coq en la década de 1990 conChristine Paulin-Mohring , quien desarrolló el asistente de prueba de Coq . Inventó la estructura de datos zip en 1996. Fue Jefe de Relaciones Internacionales de INRIA en 1996–2000. Diseñó el juego de herramientas Zen Computational Linguistics en 2000–2004.

Organizó el Instituto de Fundamentos Lógicos de la Programación Funcional durante el Año de la Programación en la Universidad de Texas en Austin en la primavera de 1987. Organizó el Coloquio "Probar y Mejorar Programas" en Arc-et-Senans en 1975, la 5ª Conferencia Internacional on Automated Deduction (CADE) en Les Arcs en 1980, el Logic in Computer Science Symposium (LICS) en París en 1994, y el First International Symposium in Sanskrit Computational Linguistics en 2007. Fue coordinador de los proyectos europeos ESPRIT Logical Frameworks, luego TIPOS, de 1990 a 1995.

Ha realizado importantes contribuciones a la teoría de la unificación y al desarrollo de lenguajes de programación funcionales tipificados , en particular Caml . Más recientemente ha sido un erudito en lingüística computacional en sánscrito . [1] [2] En particular, está trabajando en las máquinas de Eilenberg y en la estructura formal del sánscrito . [3] Es webmaster del Sánscrito Heritage Site. [4]