mini|Gérard Huet, 1978 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)Mathematics Genealogy Project 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).Huet The undecidability of unification in third order logic, Information and Control, Band 22, 1973, S. 257–267, Abstract. Unabhängig 1972 von Lucchesi. Er entwickelte aber einen Algorithmus zur Suche nach Unifizierern.Huet A Unification Algorithm for Typed Lambda-Calculus, Theoretical Computer Science 1 (1975), 27–57Huet Higher order unification 30 years later, Proc. 15th Int. Conf. Theorem Proving in Higher Order Logics, Springer Verlag 2002, S. 3–12 Er befasst sich mit automatischen Beweissystemen, konstruktiver Mathematik und Beweisassistenten (wie Coq).Coq und diversen anderen Bereichen der theoretischen Informatik und mit Software-Engineering.
1980 veröffentlichte er eine grundlegende Arbeit zu Reduktionssystemen.Huet Confluent Reductions I: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), Band 27, 1980, S. 797–821 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.Er ist Webmaster des Sanskrit Heritage Site und einer der Leiter der
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 Homepage
Einzelnachweise
Kategorie:Informatiker Kategorie:Mitglied der Académie des sciences Kategorie:Mitglied der Academia Europaea Kategorie:Franzose Kategorie:Geboren 1947 Kategorie:Mann