Gérard Huet was born on July 7th 1947 in Bourges, France. He has been married to Dr Anne Schroeder and they have three children (Isabelle, Olivier and Florence).
He obtained in 1969 his Engineer Diploma from Ecole Nationale Supérieure de l’Aéronautique et de l’Espace, and in parallel a Maîtrise d’Informatique from University of Paris. In 1970 he obtained an MS, and in 1972 a Ph.D. in Computer Science from Case Western Reserve University, Cleveland, Ohio. His MS thesis concerned theorem proving in first order logic with equality, whereas his Ph.D. concerned higher order logic in Church’s type theory, for which he proposed a unification algorithm used as constraint solver in conjonction with a resolution system.
He entered the French Institut de Recherche en Informatique et Automatique (IRIA to become INRIA) in 1972 as a researcher. He pursued research both in Theoretical Computer Science, and in Software Engineering. In 1976 he obtained his Thèse d’Etat from University Paris 7 on unification theory. He worked with Gilles Kahn on the design and implementation of the Mentor Structured Editor from 1974 to 1978. He then worked on Equational Logic and Term Rewriting Systems, and on the Canonical Solver KB with Jean-Marie Hullot. In 1979-80 he was visiting researcher at SRI International, and in 1982 he started the Formel project at INRIA in Rocquencourt, with his colleague Guy Cousineau from University Paris 7 and the Laboratoire d’Informatique of Ecole Normale Supérieure. This collaborative effort led to the functional programming language Caml, later redesigned by Xavier Leroy as Caml Light then Objective Caml. In 1985 he worked with Thierry Coquand on the design of the Calculus of Constructions, a higher-order constructive proof theory, for which he defined an execution model, the Constructive Engine.
He spent the year 1985-1986 as Invited Professor at Carnegie Mellon University, where he taught a course on Formal Structures for Computation and Deduction. In 1988 he created the Coq project with Christine Paulin-Mohring from Laboratoire d’Informatique du Parallélisme at Ecole Normale Supérieure de Lyon. This collaborative effort led to the Coq Proof Assistant. During the 90's he worked on various areas at the border between fundamental informatics and mathematical logic.
From 2000 his main interest has been Computational Linguistics. He is the author of a Sanskrit-French hypertext dictionary, and developed various tools for the phonetical, morphological and lexical analysis of Sanskrit, such as the Zen toolkit. From this research evolved a new paradigm for relational programming, inspired from Samuel Eilenberg's X-machines.
He was Professor at the University of Orsay in 1975-76. He was Visiting Professor at the Asian Institute of Technology in Bangkok in the Winter 1986. 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 taught courses at the Marktoberdorf Summer School in 1986, 1989 and 1995, at the Toulouse Summer School on Logic and Informatics in 1989, at the Ecole du Greco de Programmation in 1991, 1992, 1993 and 1994. He organised CEFIPRA workshops at IIT Kanpur in 1990 and 1995, and a series of Winter schools at Institute of Physics in Bhubaneshwar (Orissa) in 1999, 2000 and 2002. He taught at the 2002 ESSLLI Summer School in Trento. He taught a graduate course "Linguistic Modelling using Logical and Computational Tools" at MPRI (Master Parisien de Recherche en Informatique) in 2005-2007.
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, and the Logic in Computer Science Symposium (LICS) in Paris in 1994.
He was Program Chair and local organizer of the First International Sanskrit Computational Symposium in Paris in October 2006, co-Program Chair of the Third International Sanskrit Computational Symposium in Hyderabad in January 2009, member of the Program Committee of the second one at Brown University in 2008 and of the fourth one at JNU in Delhi in 2010. He is founding member of the Steering Committee of this series of symposia. He is member of the Advisory Committee of the International Conference on Distributed Computing and Internet Technologies (ICDCIT); he was General Chair of ICDCIT-2007 in Bangalore.
He was Editor of the books “Logical Foundations of Functional Programming’’ (1990), “Logical Frameworks’’(1991) , and “Logical Environments’’ (1993). He co-edited the Springer Verlag Lecture Notes Volumes 5402 and 5406 (2009) gathering the edited proceedings of the International Sanskrit Computational Symposia 1+2 and 3. He is also co-editor of the book “From Semantics to Computer Science. Essays in Honour of Gilles Kahn.
Cambridge University Press, 2009.’’
He is the author of more than 100 research publications. He directed 20 doctoral theses, and took part to more than 120 thesis committees internationally. More details, and a complete list of publications, is available from his personal home page.
He was coordinator of the European ESPRIT Basic research actions Logical Frameworks, then TYPES, from 1990 to 1995. He is principal investigator on the French side of a joint team on Sanskrit Computational Linguistics between INRIA and University of Hyderabad since 2007. He has been editor of many international journals, and stood on numerous Program Committees of International Conferences.
He was member of INRIA Evaluation Committee from 1989 to 1995, and of the CNRS Scientific Evaluation Boards of the Laboratories LIFL in Lille (1990-1992), LIP in Lyon (1993-1994) and LaBRI in Bordeaux (1998-1999). He headed the International Relations Office of INRIA from 1997 to 2000. He has been member of the board of UNU/IIST from 1999 to 2003, and of the University Paris 7 from 2002 to 2005. He has been member of the International Advisory Board of TRDCC (Tata Consultancy Services, Pune, India) from 2002 to 2005. He was member of the International Advisory Board of NII (National Institute of Informatics, Tokyo, Japan) in 2005-2006. He was member of the Scientific Council of the GIS SARIMA (fostering African Mathematics and Computer Science) in 2004-2008. He was Scientific Director of the INRIA-MSR Joint Laboratory in Orsay from February to July 2006. He has been member of the Scientific Council of CEFIPRA since 2012.
He has been Directeur de Recherches de Classe Exceptionnelle at INRIA from 1989 to 2013, and has now the Emeritus status. He was elected Member of Academia Europaea in 1989, and Membre de l’Académie des Sciences in 2002. He received the Herbrand Award for his work on Computational Logic in 1998. He received a degree of Doctor of Technology honoris causa from Chalmers University in Göteborg (Sweden) in 2004. He received in July 2009 the prestigious EATCS Award. In 2011 he was the first recipient of the Inria Grand Prix. He was awarded the ACM-Sigplan Programming Languages Software Award in 2013 and the ACM Software Award in 2014 for his work on the Coq proof assistant
G. Huet's publications are listed in his publication page. Most of his recent publications can be downloaded from there.