EATCS Award 2009
The EATCS Award is awarded in recognition of a distinguished career in theoretical computer science. The Committee, consisting of Catuscia Palamidessi (Chair), Paul Spirakis and Emo Welzl in charge of evaluating the nominations to the 2009 EATCS Award has come to the decision to propose Gérard Huet as the candidate for the 2009 EATCS Award in view of the excellent research contributions to theoretical computer science produced throughout his outstanding scientific career. The Committee unanimously shares the motivations contained in the nomination letter. The proposal has been unanimously approved by the EATCS Council. The Award will be assigned during a ceremony that will take place in Rhodes (Greece) during ICALP2009 (July 5-12, 2009).
Nomination of Gerard Huet for the EATCS Award 2009
Gérard Huet has made numerous, enduring advances in the foundations of computer science and has been a central figure in several important software systems. He has also had a remarkably active and successful academic and professional life. His distinguished career in theoretical computer science has exerted considerable influence on not only the field but also the many students and colleagues that he has directly influenced.
A hallmark of Huet research is his talent for taking highly technical material and providing it with a clear and deep analysis. For example, in his paper on the unification of typed lambda-terms (in the first volume of TCS, 1975), Huet took a difficult topic, reshaped and redefined it, and left a solution so well developed that it took more than 15 years of active research before any one saw a need to extend it. Since that first major result, he has repeated this performance numerous times.
Equally characteristic of Huet's research is the intimate connections he maintains between theoretical computer science topics and their effective implementation. He was one of the first computer scientists who was able to move between these two domains and who felt that there was no option to doing so: these two topics were absolutely needed to inform each other.
Huet was a leader in the general areas of logical frameworks and constructive typed theories. Thanks in large part to his achievements and efforts, formal mathematics has taken huge strides and is starting to have an impact on the wider world. He has worked extensively at disseminating his view of this bold new world of formalized reasoning: for example, he has organized numerous summer schools and given countless invited talks and tutorials. Many researchers in France and elsewhere count themselves as students of Huet even if they were never formally his PhD advisee.
Principal Scientific Contributions
We list and briefly describe some of the many contributions made by Gérard Huet.
In the early 70's, Huet developed both resolution and unification for higher-order logic: these results have became the core of several modern systems that perform deduction in higher-order logic.
Huet has done fundamental research in the areas of rewriting and Knuth-Bendix completion. His writings in this area are extensive and elegant. - Between 1982 and 1989, Huet directed and contributed to the design and implementation of the CAML functional programming language. That language and its descendants have given academics and industries an efficient and well structured programming language.
In the 1990s, Huet and his students designed and built the first version of the Coq proof assistant. Today, Coq is one of the most used and trusted platforms for formalized mathematics and formal methods.
Huet has a broad culture inside and outside of computer science. He has made, for example, important contributions in other areas as well: he is the author of "executable" lecture notes; he is the designer of the Zipper data structure; and he has built the Zen toolbox for phonological and morphological segmentation and labeling of Sanskrit.
In 1972, Huet received his PhD in Computer Science from Case Western Reserve University, Ohio, USA and in the same year, he started as a researcher at IRIA (which later became INRIA), a position that he has maintained since then. In 1976 he obtained his Thθse d'Etat from University Paris 7. In addition to being a researcher at INRIA, he has been a Professor at the University of Orsay in 1975-76; an Invited Professor at Carnegie Mellon University during 1985-1986; and a Visiting Professor at the Asian Institute of Technology in Bangkok in 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 organized 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 has taught at a number of summer schools, including the Marktoberdorf Summer School, the Toulouse Summer School on Logic and Informatics, the Ecole du Greco de Programmation, and the ESSLLI Summer School. He was the conference organizer for the 5th International Conference on Automated Deduction (CADE) in Les Arcs in 1980 and for the Logic in Computer Science Symposium (LICS) in Paris in 1994.
He has edited three books and authored more than 80 research papers. He has also directed 19 doctoral thesis (including T. Coquand, G. Dowek, C. Paulin-Mohring, and X. Leroy) and took part to more than 100 thesis committees internationally. Huet was also the coordinator of the ESPRIT European projects Logical Frameworks and TYPES from 1990 to 1995.
Huet has received a number of honors and awards to date. He has been ``Directeur de Recherches de Classe Exceptionnelle'' at INRIA since 1989. He was elected a Member of Academia Europaea in 1989 and a Member of the Academy of Sciences of the Institute of France in 2002. He received the Herbrand Award for his work on Computational Logic in 1998 and received the degree of Doctor of Technology honoris causa from Chalmers University in Gφteborg (Sweden) in 2004.