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)[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

Homepage

Einzelnachweise

Mathematics Genealogy Project
Huet The undecidability of unification in third order logic, Information and Control, Band 22, 1973, S. 257–267, Abstract. Unabhängig 1972 von Lucchesi.
Huet A Unification Algorithm for Typed Lambda-Calculus, Theoretical Computer Science 1 (1975), 27–57
Huet Higher order unification 30 years later, Proc. 15th Int. Conf. Theorem Proving in Higher Order Logics, Springer Verlag 2002, S. 3–12
Coq
Huet Confluent Reductions I: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), Band 27, 1980, S. 797–821
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@2

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[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@2