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 .
Biografía
Gérard Huet se graduó en la Universidad Denis Diderot (París VII), la Universidad Case Western Reserve y la Universidad de París . [ cita necesaria ]
Es director senior de investigación del INRIA , miembro de la Academia Francesa de Ciencias y miembro de la Academia Europaea . Anteriormente fue profesor visitante en el Instituto Asiático de Tecnología en Bangkok , profesor visitante en la Universidad Carnegie Mellon e investigador invitado en SRI International .
Es 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 en 1974-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 con Christine Paulin-Mohring , quien desarrolló el asistente de prueba Coq . Inventó la estructura de datos de cremallera en 1996. Fue Jefe de Relaciones Internacionales de INRIA en 1996-2000. Diseñó el conjunto de herramientas de Lingüística Computacional Zen 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 “Probando y Mejorando Programas” en Arc-et-Senans en 1975, la V Conferencia Internacional sobre Deducción Automatizada (CADE) en Les Arcs en 1980, el Simposio de Lógica en Informática (LICS) en París en 1994, y el Primer Simposio Internacional de Lingüística Computacional Sánscrita en 2007. Fue coordinador de los proyectos europeos ESPRIT Marcos Lógicos, 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 estudioso de la 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 el webmaster del sitio del patrimonio sánscrito. [4]
Huet recibió el Premio Herbrand en 1998 [5] y el Premio EATCS en 2009. [6]
Publicaciones
- Le Projet prévision-réalisation des vols , Société d'informatique, de conseils et de recherche opérationnelle (SINCRO), París, 1970. Registro WorldCat
- Spécifications pour une base commune de données , SINCRO, París, 1971. Registro WorldCat
- Gérard P. Huet (1973). "Una mecanización de la teoría de tipos" (PDF) . En Nils J. Nilsson (ed.). Proc. 3° Int. Conferencia conjunta. sobre Inteligencia Artificial (IJCAI) . Guillermo Kaufmann. págs. 139-146.
- Gérard P. Huet (1973). "La indecidibilidad de la unificación en la lógica de tercer orden". Información y Control . 22 (3): 257–267. doi :10.1016/s0019-9958(73)90301-x.
- La Gestion des données dans les systèmes informatiques , École supérieure d'électricité, Malakoff, 1974. Registro WorldCat
- "Un algoritmo de unificación para cálculo lambda tipificado", Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
- Gérard Huet (septiembre de 1976). Resolución de ecuaciones en idiomas de orden 1,2,...ω (Ph.D.). Universidad de París VII.
- Gérard Huet, Bernard Lang (1978). "Demostración y aplicación de transformaciones de programas expresadas con patrones de segundo orden". Acta Informática . 11 : 31–55. doi :10.1007/bf00264598. S2CID 27669838.
- Gérard Huet, DS Lankford (marzo de 1978). Sobre el problema de la detención uniforme de los sistemas de reescritura de términos (PDF) (Reporte técnico). IRIA. pag. 8. 283.
- G. Huet, JM Hullot (octubre de 1980). "Pruebas por inducción en teorías ecuacionales con constructores". 21 Ana. Síntoma. sobre los fundamentos de la informática (PDF) . vol. 25. IEEE. págs. 96-107. doi :10.1016/0022-0000(82)90006-X. S2CID 9214469.
- G. Huet, DC Oppen (enero de 1980). Ecuaciones y reglas de reescritura: una encuesta (PDF) (Reporte técnico). Universidad de Stanford, Departamento de informática p. 52. STAN-CS-80-785.
- Gérard Huet (1981). "Una prueba completa de la corrección del algoritmo de finalización de Knuth-Bendix". J. Computación. Sistema. Ciencia . 23 (1): 11–21. doi : 10.1016/0022-0000(81)90002-7 .
- Gérard Huet (mayo de 1986). Estructuras formales para computación y deducción. Escuela Internacional de Verano sobre Lógica de Programación y Cálculo de Diseño Discreto. Archivado desde el original el 14 de julio de 2014 . Consultado el 19 de junio de 2014 .
- Gérard Huet (1988). K. Fuchi y M. Nivat (ed.). Principios de Inducción Formalizados en el Cálculo de Construcciones (PDF) . Holanda del Norte. págs. 205-216. Archivado desde el original (PDF) el 1 de julio de 2015 . Consultado el 19 de junio de 2014 .
- Gérard Huet (agosto de 1993). Teoría residual en λ-Cálculo: un desarrollo formal (PDF) (Reporte técnico). INRIA. 2009. Archivado desde el original (PDF) el 1 de julio de 2015 . Consultado el 19 de junio de 2014 .
- Huet, médico de cabecera (1996). Ganzinger, Harald (ed.). Asistente de Prueba de Diseño (conferencia invitada) . LNCS. vol. 1103. Springer-Verlag. pag. 153.
- Gérard Huet, H. Laulhère (septiembre de 1997). "Transductores de estados finitos como árboles de Böhm regulares" (PDF) . En M. Abadi y T. Ito (ed.). Aspectos teóricos del software informático . LNCS. vol. 1281. Saltador. págs. 604–610. Archivado desde el original (PDF) el 22 de diciembre de 2014 . Consultado el 19 de junio de 2014 .
- Gérard Huet (1998). "Árboles Böhm normales" (PDF) . Matemáticas. Estructura. En Comp. Ciencia . 8 (6): 671–680. doi :10.1017/s0960129598002643. S2CID 15752309. Archivado desde el original (PDF) el 24 de enero de 2016 . Consultado el 19 de junio de 2014 .
- Gérard Huet (2002). "Unificación del Orden Superior 30 años después" (PDF) . En V. Carreño y C. Muñoz y S. Tahar (ed.). Actas de la 15ª Conferencia Internacional TPHOL . LNCS. vol. 2410. Saltador. págs. 3–12.Posdata
- Gérard Huet (2003). Fairouz Kamareddine (ed.). Contextos lineales y functor compartido: técnicas de computación simbólica (PDF) . Kluwer. Archivado desde el original (PDF) el 1 de julio de 2015 . Consultado el 19 de junio de 2014 .
Referencias
- ^ Pawan Goyal, Gérard Huet (enero de 2013). "Análisis de integridad de un lector de sánscrito" (PDF) . Actas del Quinto Simposio Internacional sobre Lingüística Computacional Sánscrita, Mumbai . Archivado desde el original (PDF) el 14 de julio de 2014 . Consultado el 19 de junio de 2014 .
- ^ Gérard Huet, Pawan Goyal (diciembre de 2013). "Diseño de una interfaz sencilla para la anotación de corpus en sánscrito" (PDF) . Actas, ICON13, Hyderabad . Archivado desde el original (PDF) el 14 de julio de 2014 . Consultado el 19 de junio de 2014 .
- ^ Gerard Huet. Archivado el 12 de septiembre de 2008 en la Wayback Machine.
- ^ Sitio del patrimonio sánscrito
- ^ "Premio Herbrand por contribuciones distinguidas al razonamiento automatizado". Archivado desde el original el 7 de febrero de 2015 . Consultado el 7 de febrero de 2015 .
- ^ Premio de la Asociación Europea de Informática Teórica
enlaces externos
- - Sitio de patrimonio sánscrito: [1]. Consultado el 29 de julio de 2020.
- - Dictionnaire Héritage du Sanscrit : versión pdf.descargable, actualizada periódicamente por el autor: [2]. Consultado el 29 de julio de 2020.
- - Versión DICO online (página de inicio): [3]. Consultado el 29 de julio de 2020.
