Gérard Huet

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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

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)[1] 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).[2] Er entwickelte aber einen Algorithmus zur Suche nach Unifizierern.[3].[4] Er befasst sich mit automatischen Beweissystemen, konstruktiver Mathematik und Beweisassistenten (wie Coq).[5] und diversen anderen Bereichen der theoretischen Informatik und mit Software-Engineering.

1980 veröffentlichte er eine grundlegende Arbeit zu Reduktionssystemen.[6]

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.[7]

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.

Weblinks[Bearbeiten]

Einzelnachweise[Bearbeiten]

  1. Mathematics Genealogy Project
  2. Huet The undecidability of unification in third order logic, Information and Control, Band 22, 1973, S. 257-267, Abstract. Unabhängig 1972 von Lucchesi.
  3. Huet A Unification Algorithm for Typed Lambda-Calculus, Theoretical Computer Science 1 (1975), 27-57
  4. Huet Higher order unification 30 years later, Proc. 15th Int. Conf. Theorem Proving in Higher Order Logics, Springer Verlag 2002, S. 3-12
  5. Coq
  6. Huet Confluent Reductions I: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), Band 27, 1980, S. 797 – 821
  7. Er ist Webmaster des Sanskrit Heritage Site und einer der Leiter der Sanscrit Library