Gérard Huet

from Wikipedia, the free encyclopedia

Gérard Huet (born July 7, 1947 in Bourges ) is a French computer scientist.

Life

Huet received his doctorate in 1972 from Case Western Reserve University with George Ernst (Ph. D., topic: Constrained Resolution: A Complete Method for Higher-Order Logic) and in 1976 at the University of Paris VII with Maurice Nivat (Résolution d'équations dans des langages d'ordre 1, 2, ..., omega) He was a professor at the University of Paris VII (Denis Diderot). He also conducted research at the Institut national de recherche en informatique et en automatique (INRIA).

In 1973 he proved the undecidability of the problem of unification in 3rd order logic and higher level ( type theory ). But he developed an algorithm to search for unifiers. He deals with automatic proof systems, constructive math, and proof assistants (like Coq ). and various other areas of theoretical computer science and software engineering.

In 1980 he published a fundamental paper on reduction systems . From 1984 to 1985 he developed the ML variant Caml at INRIA. He also studies the formal linguistic structure of Sanskrit and computer linguistics of Sanskrit.

In 1998 he received the Herbrand Award , in 2009 the EATCS Award and in 2013 the ACM Software System Award together with several IT specialists .

He is a member of the Académie des Sciences and the Academia Europaea .

Web links

Individual evidence

  1. ^ Mathematics Genealogy Project
  2. Huet The undecidability of unification in third order logic , Information and Control, Volume 22, 1973, pp. 257-267, abstract . Independent from Lucchesi in 1972.
  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, pp. 3–12
  5. ^ Coq
  6. ^ Huet Confluent Reductions I: Abstract Properties and Applications to Term Rewriting Systems , Journal of the ACM (JACM), Volume 27, 1980, pp. 797-821
  7. He is the webmaster of the Sanskrit Heritage Site and one of the directors of the Sanscrit Library ( Memento of the original from June 3, 2013 in the Internet Archive ) Info: The archive link was automatically inserted and not yet checked. Please check the original and archive link according to the instructions and then remove this notice. @1@ 2Template: Webachiv / IABot / sanskritlibrary.org