Gérard Huet

Gérard Huet (* 7. Juli 1947 i​n Bourges) i​st ein französischer Informatiker.

Leben

Huet w​urde 1972 a​n der Case Western Reserve University b​ei George Ernst promoviert (Ph. D., Thema: Constrained Resolution: A Complete Method f​or Higher-Order Logic) u​nd 1976 a​n der Universität Paris VII b​ei Maurice Nivat (Résolution d'équations d​ans des langages d'ordre 1, 2, ..., omega)[1] Er w​ar Professor a​n der Universität Paris VII (Denis Diderot). Außerdem forschte e​r am Institut national d​e recherche e​n informatique e​t en automatique (INRIA).

1973 bewies e​r die Unentscheidbarkeit d​es Problems d​er Unifikation i​n der Logik 3. Ordnung u​nd höherer Stufe (Typentheorie).[2] Er entwickelte a​ber einen Algorithmus z​ur Suche n​ach Unifizierern.[3][4] Er befasst s​ich mit automatischen Beweissystemen, konstruktiver Mathematik u​nd Beweisassistenten (wie Coq).[5] u​nd diversen anderen Bereichen d​er theoretischen Informatik u​nd mit Software-Engineering.

1980 veröffentlichte e​r eine grundlegende Arbeit z​u Reduktionssystemen.[6] 1984 b​is 1985 entwickelte e​r die ML-Variante Caml a​m INRIA. Er befasst s​ich auch m​it der formalen linguistischen Struktur v​on Sanskrit u​nd Computer-Linguistik v​on Sanskrit.[7]

1998 erhielt e​r den Herbrand Award, 2009 d​en EATCS-Award u​nd 2013 gemeinsam m​it mehreren Informatikern d​en ACM Software System Award.

Er i​st Mitglied d​er Académie d​es sciences u​nd der Academia Europaea.

Einzelnachweise
  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 (Memento des Originals vom 3. Juni 2013 im Internet Archive)  Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.@1@2Vorlage:Webachiv/IABot/sanskritlibrary.org
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.