Gérard Huet
# Gérard Huet

Gérard Huet (* 7. Juli 1947 in Bourges) ist ein französischer Informatiker.

## Leben

Huet wurde 1972 an der Case Western Reserve University bei George Ernst promoviert (Ph. D., Thema: Constrained Resolution: A Complete Method for Higher-Order Logic) und 1976 an der Universität Paris VII bei Maurice Nivat (Résolution d'équations dans des langages d'ordre 1, 2, ..., omega) Er war Professor an der Universität Paris VII (Denis Diderot). Außerdem forschte er am Institut national de recherche en informatique et en automatique (INRIA).

1973 bewies er die Unentscheidbarkeit des Problems der Unifikation in der Logik 3. Ordnung und höherer Stufe (Typentheorie). Er entwickelte aber einen Algorithmus zur Suche nach Unifizierern. Er befasst sich mit automatischen Beweissystemen, konstruktiver Mathematik und Beweisassistenten (wie Coq). und diversen anderen Bereichen der theoretischen Informatik und mit Software-Engineering.

1980 veröffentlichte er eine grundlegende Arbeit zu Reduktionssystemen. 1984 bis 1985 entwickelte er die ML-Variante Caml am INRIA. Er befasst sich auch mit der formalen linguistischen Struktur von Sanskrit und Computer-Linguistik von Sanskrit.

1998 erhielt er den Herbrand Award, 2009 den EATCS-Award und 2013 gemeinsam mit mehreren Informatikern den ACM Software System Award.

Er ist Mitglied der Académie des sciences und der Academia Europaea.

