Sites Inria

Version française



Gérard Huet is to be awarded the prestigious EATCS Award

The European Association of Theoretical Computer Science (EATCS) will present Gérard Huet with the 2009 Award on 9 July in Rhodes. This award comes in recognition of a long career dedicated to computer science punctuated with numerous breakthroughs.

By awarding Gérard Huet the EATCS Award, the scientific community is paying tribute to the brilliant career of this outstanding Inria researcher. This prize rewards scientists who have made advances in the foundations of computer science and created original and enduring solutions to complex problems.

For forty years, Gérard Huet has devoted himself to the field of formal proof - demonstrating and proving mathematical theoretical reasoning in practical terms with a view to expressing such reasoning in the form of an algorithm. With his team, he designed the Coq proof assistant which allows users to break down such forms of reasoning and prove them step by step. Software programs that result from such reasoning can then be integrated into high-security applications, such as air transport or financial transaction systems where nothing can be left to chance as regards the reliability of the computing application.

In recent years, Gérard Huet has turned his attention to another field of computing - natural language processing. He has developed algorithms allowing continuous utterances to be analysed, broken down into words and grammatically parsed. He has proved that these tools are able to resolve problems related to the segmentation of Classical Sanskrit - a complicated, phonetic and codified language of ancient India. We are also indebted to him for the first hypertext Sanskrit dictionary with integrated grammatical parsing tools.

He is a member of the French Academy of Science and the Academia Europaea and was awarded the Herbrand Award. The talents of this brilliant scientist are recognised by all. Today, it is the EATCS Association’s turn to honour him.

His scientific work

1972: in the field of demonstration theory, a sub-field of mathematical logic, Gérard Huet invented a unification algorithm for typed Lambda-Calculus which bears his name.  Among other things, this algorithm serves as a nucleus for higher-order logic programming interpreters, and also helps to recognise anaphora in natural language.

I n the Seventies: together with Gilles Kahn, Gérard Huet headed the CROAP Project which perfected the Mentor development environment for structured documents.

1979:  a pioneer in the field of equational proof by rewriting; together with Jean-Jacques Lévy, he characterised a family of recursive, sequential computation systems.

In the Eighties: he headed the Formel Project which developed the OCaml programming language. This language is widely used, particularly in the teaching of programming. Its last avatar, Objective Caml, defines a typical functional language standard suitable for the development of reliable software.

1984: alongsideThierry Coquand, Gérard Huet defined the Calculus of Constructions (the founder formalism of a powerful family of logical calculi), which enables mathematical proof to be expressed concisely.

 In the Nineties: together with Christine Paulin-Mohring, he headed the Coq Project, which developed the eponymous proof assistant. It is currently one of the most used formal mathematics development and certified software systems.

Keywords: EATCS Award Gérard Huet