Gérard Huet

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

Graduated from:
* Université Denis Diderot (Paris VII)
* Case Western Reserve University
* Université de Paris
*

His specialties are:
* Software architecture
* Design of programming languages and of proof assistants
* Project management
* International relations

He is:
* Senior research director at INRIA
* A member of the French Academy of Sciences
* A member of Academia Europaea
* Formerly a Visiting Professor at Asian Institute of Technology, Bangkok
* Formerly a Visiting Professor at Carnegie-Mellon University
* Formerly a Guest Researcher at SRI International

He was the author of a unification algorithm for simply typed lambda-calculus, and of a complete proof method for Church's theory of types (Constrained Resolution). He worked on the Mentor program editor in 1974-1977 with Gilles Kahn. He worked on the KB equational proof system in 1978-1984 with Jean-Marie Hullot. He led the Formel project in the 80's, which developed the Caml programming language. He designed the Calculus of Constructions in 1984 with Thierry Coquand. He led the Coq project in the 90's with Christine Paulin, which developed the Coq proof assistant. He invented the Zipper data stucture in 1996. He was Head of International Relations for INRIA in 1996-2000. He designed the Zen Computational Linguistics toolkit in 2000-2004. He is currently working on a Computational

He organized the Institute of Logical Foundations of Functional Programming during the Year of Programming at the University of Texas in Austin in Spring 1987. He organised the Colloquium “Proving and Improving Programs’’ in Arc et Senans in 1975, the 5th International Conference on Automated Deduction (CADE) in Les Arcs in 1980, the Logic in Computer Science Symposium (LICS) in Paris in 1994, and the First International Symposium in Sanskrit Computational Linguistics in 2007. He was coordinator of the ESPRIT European projects Logical Frameworks, then TYPES, from 1990 to 1995.

He has made major contributions to the theory of unification and to the development of typed functional programming languages, in particular CAML. More recently he has been a student of computational linguistics in Sanskrit and he is webmaster of the [http://sanskrit.inria.fr/ Sanskrit Heritage Site] . In particular, he is working on Eilenberg machines and on the formal structure of Sanskrit. [ [http://www.linkedin.com/profile?viewProfile=&key=10426742 Gérard Huet] ]

Publications

* [http://mathgate.info/cebrown/notes/huet75.php "A Unification Algorithm for Typed Lambda-Calculus", Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57]
* [http://pauillac.inria.fr/~huet/PUBLIC/Hampton.pdf "30 Years of Higher-Order Unification", Gérard Huet, TPHOL 2002, INRIA]
*"Le Projet prévision-réalisation des vols", SINCRO, Paris, 1970.
*"Spécifications pour une base commune de données", SINCRO, Paris, 1971.
*"A Mechanization of type theory", LABORIA, Rocquencourt, 1973.
*"La Gestion des données dans les systèmes informatiques", École supérieure d'électricité, Malakoff, 1974.

ee also

* Unification
* CAML

References

External links

* [http://pauillac.inria.fr/~huet/ Huets's home page]
* [http://pauillac.inria.fr/~huet/ Notice biographique de l'INRIA]
*PDF| [http://sanskrit.inria.fr/Dico.pdf Gérard Huet "Héritage du sanskrit" dictionnaire sanskrit-français] |3.32 MB (428 pages, version du 5 avril 2007 consultée en ligne)
* [http://fr.wikipedia.org/wiki/G%C3%A9rard_Huet French Wikipedia entry]