Gérard Huet
| Gérard Huet | |
|---|---|
| Born |
7 July 1947 Bourges |
| Nationality | French |
| Fields | Mathematics |
| Alma mater |
Case Western Reserve University University of Paris |
| Doctoral advisor | George Ernst Maurice Nivat |
| Doctoral students |
Thierry Coquand François Fages Jean-Marie Hullot Xavier Leroy Christine Paulin-Mohring Didier Rémy |
Gérard Pierre Huet (born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and to the theory of computation.
Gérard Huet graduated from the Université Denis Diderot (Paris VII), Case Western Reserve University, and the Université de Paris.
He is senior research director at INRIA, a member of the French Academy of Sciences, and a member of Academia Europaea. Formerly he was a visiting professor at Asian Institute of Technology in Bangkok, a visiting professor at Carnegie Mellon University, and a guest researcher at SRI International.
He is 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 1980s, which developed the Caml programming language. He designed the Calculus of Constructions in 1984 with Thierry Coquand. He led the Coq project in the 1990s with Christine Paulin, who developed the Coq proof assistant. He invented the zipper data structure in 1996. He was Head of International Relations for INRIA in 1996–2000. He designed the Zen Computational Linguistics toolkit in 2000–2004.
...
Wikipedia