Logic List Mailing Archive

Gerard Huet wins 2009 EATCS Award

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 Grard 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 ICALP (July 5-12, 2009).

Read more:

*
http://www.eatcs.org/index.php/component/content/article/1-news/547-eatcs-a
ward-2009-

* http://icalp09.cti.gr

=========================
=========================
======================
Nomination of Gerard Huet for the EATCS Award 2009
=========================
=========================
======================

Grard 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
Grard 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.

=========================
=========================
======================