Gérard Huet
Pour les articles homonymes, voir Huet.
| Naissance | |
|---|---|
| Nationalité | |
| Formation | Université Paris-Diderot (doctorat) (jusqu'en ) École nationale supérieure de l'aéronautique et de l'espace (en) Université Case Western Reserve Faculté des sciences de Paris |
| Activités |
| A travaillé pour | |
|---|---|
| Membre de | |
| Maître | George Ernst (d) |
| Directeur de thèse | |
| Site web | |
| Distinctions |
Gérard Huet (né le à Bourges) est un logicien et chercheur en informatique théorique français. Il est membre de l’Académie des sciences de l’Institut de France, dans la section Sciences mécaniques et Informatique.
Biographie[modifier | modifier le code]
Gérard Huet est directeur de recherche émérite (de classe exceptionnelle) à l'Institut national de recherche en informatique et en automatique (Inria) et membre de l'Académie des sciences. Il a obtenu le prix de l'European Association for Theoretical Computer Science en 2009[1],[2] et a été le premier récipiendaire du Grand Prix Inria en 2011[3].
Il est également l'auteur d'un dictionnaire sanskrit-français consultable en ligne, The Sanskrit Heritage Dictionary.
Gérard Huet obtint son diplôme d'ingénieur civil de l'aéronautique et de l’espace (Sup’Aéro) en 1969, en même temps qu'une maîtrise d'informatique de la Faculté des sciences de Paris. Parti aux États-Unis se spécialiser en intelligence artificielle, il obtint un master en 1970 et un Ph.D. en Computer Science en 1972 à l'université Case Western Reserve à Cleveland. Son master portait sur la réalisation d'un démonstrateur interactif pour la logique de 1er ordre avec égalité. Son Ph.D. définissait une procédure de semi-décision complète pour la logique d'ordre supérieur (théorie des types de Church), où la recherche de preuves est guidée par un calcul de contraintes d'unification. Il établissait l’indécidabilité de l’unification d’ordre 3, et un semi-algorithme d’unification dans le lambda-calcul typé qui porte son nom.
Rentré en France en 1972, il obtint un poste de chercheur à l’IRIA (Institut de recherche en informatique et en automatique) à Rocquencourt. Il y travailla avec Gilles Kahn à la conception et à la réalisation de l’éditeur structuré Mentor de 1974 à 1978. En 1976, il obtint son doctorat en mathématiques à l'université Paris-Diderot. Sa thèse portait sur l’algorithmique de l’unification, un procédé fondamental de logique mathématique[4]. Il orienta ensuite sa recherche vers la logique de l’égalité et les systèmes de réécriture avec Jean-Marie Hullot, ce qui donna lieu au système KB de réécriture canonique. Invité au Stanford Research Institute en 1979-1980, il rédigea avec Derek Oppen la monographie Equations and Rewrite rules. Avec Jean-Jacques Lévy, il dégagea la notion de système de réécriture fortement séquentiel.
De retour à l’IRIA (qui allait devenir l’INRIA, Institut national de recherche en informatique et en automatique), il démarra l’équipe-projet Formel en 1982 avec son collègue de l'université Paris-Diderot Guy Cousineau, en collaboration avec le laboratoire d’informatique de l’ENS. Cet effort donna naissance au langage de programmation fonctionnel Caml, qui sera plus tard repensé par Xavier Leroy comme Caml-light puis OCaml. En 1984-1985, il travailla avec Thierry Coquand à la conception du Calcul des constructions, système logique basé sur un lambda-calcul typé avec types dépendants, dans l’esprit du langage Automath de Nicolas de Bruijn. Thierry Coquand prouva dans sa thèse la cohérence du calcul, tandis que Gérard Huet posait avec la Constructive Engine les bases d’une mécanisation du calcul, ancêtre du système Coq[5].
Professeur invité à l’université Carnegie Mellon de Pittsburgh en 1985-1986, il enseigna le cours « Formal Structures for Computation and Deduction » qui inspirera plus tard la conférence FSCD. En 1988, il démarra l’équipe-projet Coq avec Christine Paulin-Mohring du Laboratoire d’informatique du parallélisme de l'École normale supérieure de Lyon. Cet effort donna naissance à l’assistant de preuves Coq.
Dans les années 1990, Gérard Huet travailla à divers problèmes de logique mathématique et d’informatique théorique, tout en dirigeant l’effort Coq. Il inventa la structure de données Zipper en 1996[6].
De 1997 à 2000, il assuma la responsabilité de délégué aux relations internationales de l’INRIA.
Depuis 2000, il se consacre au traitement de la langue naturelle, et notamment du sanskrit. Il est l’auteur du premier dictionnaire hypertexte Sanskrit-Français[7], le Dictionnaire Héritage du Sanskrit. Il a développé la bibliothèque Zen, ensemble de modules OCaml permettant le traitement morpho-phonétique de la langue, à l’aide d’automates décorés donnant une représentation efficace de lexiques et de transducteurs rationnels. Ceci permet notamment de segmenter le Sanskrit par inversion du sandhi. Cette technologie a donné naissance à la notion de Machine d’Eilenberg[8] Effective, développée dans le travail de thèse de Benoît Razet. Depuis 2004, le site Sanskrit Heritage fournit des outils de segmentation, analyse morphologique et gestion de corpus du sanskrit, grâce notamment à une interface graphique développée en collaboration avec Pawan Goyal. Ce logiciel est disponible sur le Gitlab Inria en open source[9].
Depuis 2013, Gérard Huet est directeur de recherches émérite Inria.
Distinctions[modifier | modifier le code]
Gérard Huet a été élu correspondant de l’Académie des sciences en 1990, puis membre en 2002, dans la section Sciences mécaniques et informatiques [10]. Il est membre de l'Academia Europaea depuis 1989 [11]. Il est Membre du Comité National Français d'Histoire et de Philosophie des Sciences.
Il reçoit le Herbrand Award pour son travail en Computational Logic en 1998[12]. La Chalmers University de Göteborg lui décerna un Doctorat Honoris Causa en 2004. Il reçut le EATCS Award[13] en 2009. En 2011 il fut le premier récipiendaire du Grand Prix Inria[14]. Il reçoit l’ACM-Sigplan Programming Languages Software Award[15] et l'ACM Software System Award en 2013 pour sa contribution à l’assistant de preuves Coq.
Décorations[modifier | modifier le code]
- Par décret présidentiel du , il a été fait Chevalier de la Légion d'honneur[16], mais ne l'a pas reçue à ce jour (2019).
Publications[modifier | modifier le code]
Il est l'auteur de très nombreuses publications scientifiques internationales[17].
Références[modifier | modifier le code]
- (en) EATCS Award 2009.
- Annonce sur le site de l'INRIA.
- Grand prix Inria.
- « Algorithme de l'unification »
- « Travaux scientifiques »
- « Zipper »
- « Dictionnaire Sanskrit »
- « Machine d'Eilenberg »
- « Biographie »
- « Académie des sciences »
- « Academia europaea »
- « Herbrand Award »
- « EATC Award »
- « Grand Prix INRIA »
- « ACM-Sigplan Programming Languages Software Award »
- Décret du 12 juillet 2013 portant promotion et nomination
- « Publications »
Liens externes[modifier | modifier le code]
- Site officiel
- Ressources relatives à la recherche :
- Page personnelle de Gérard Huet
- Page de Gérard Huet sur le site de l'Académie des sciences
- (fr + en) , Dictionnaire Héritage du Sanscrit:
