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 doctorat 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 doctorat 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-DiderotGuy 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
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 prix Herbrand pour son travail en Computational Logic en 1998[12]. L'université Chalmers de Göteborg lui décerne un doctorat honoris causa en 2004. Il reçut le EATCS Award[13] en 2009. En 2011 il est le premier récipiendaire du grand prix Inria[14]. Il reçoit l’ACM-Sigplan Programming Languages Software Award[15] et le prix ACM Software System en 2013 pour sa contribution à l’assistant de preuves Coq.
