Sites Inria

English version

Distinction

26/06/2009

Gérard Huet reçoit le prestigieux prix EATCS

Le 9 juillet prochain à Rhodes, Gérard Huet recevra le prix « Award 2009 » de l'association European Association for Theoretical Computer Science (EATCS). Ce prix vient récompenser une longue carrière dédiée à l'informatique et ponctuée par de nombreuses découvertes.

À travers le prix EATCS, la communauté scientifique salue la brillante carrière de Gérard Huet, chercheur d'excellence de l’INRIA. Ce prix récompense les scientifiques qui ont su faire avancer l'informatique fondamentale et apporter des solutions originales et durables à des problèmes complexes.

Pendant 40 ans, Gérard Huet s'est consacré au domaine de la preuve formelle : démontrer et prouver concrètement un raisonnement théorique en mathématiques en vue de sa transformation en algorithme. Avec son équipe, il a conçu l'assistant de preuves Coq qui permet à l'utilisateur de découper ces raisonnements et de les démontrer étape par étape. Les logiciels issus de ces raisonnements peuvent alors intégrer des applications de haute sécurité. Par exemple, dans les transports aériens ou les transactions financières, où la fiabilité d'une application informatique ne doit rien laisser au hasard.

Ces dernières années, Gérard Huet s'est tourné vers un autre domaine de l'informatique : le traitement de la langue naturelle. Il a ainsi mis au point des algorithmes permettant l'analyse d'une énonciation continue, son découpage en mots, et son analyse grammaticale. Il a montré que ces outils permettaient de résoudre le problème de segmentation du sanskrit classique, langue savante, phonétique et codifiée, de l'Inde antique. On lui doit ainsi le premier dictionnaire hypertexte du sanskrit qui intègre des outils d'analyse grammaticale.

Membre de l'Académie des sciences, de l'Academia Europaea, titulaire du Prix Herbrand... Tous ont reconnu les talents de ce brillant scientifique. Aujourd’hui, c’est au tour de l'association EATCS de l’honorer.

Son parcours scientifique

1972 : Dans le domaine de la théorie de la démonstration, sous-domaine de la logique mathématique, Gérard Huet invente un algorithme d'unification en théorie des types qui porte son nom. Cet algorithme sert notamment de noyau aux interprètes de programmation logique d'ordre supérieur mais aussi à la reconnaissance des anaphores en langue naturelle.

 Années 70 :  Gérard Huet dirige avec Gilles Kahn le projet CROAP qui a mis au point l'environnement de développement de documents structurés Mentor.

 1979 :  Pionnier du domaine des preuves équationnelles par réécriture, il caractérise, avec Jean-Jacques Lévy, une famille de systèmes de calcul récursifs fortement séquentiels.

 Années 80 :  Il dirige le projet Formel, qui a développé le langage de programmation Ocaml. Ce langage est utilisé à grande échelle notamment pour l'enseignement de la programmation. Le dernier avatar, Objective Caml, définit un standard de langage fonctionnel typé, approprié au développement de logiciels sûrs.

 1984 : En collaboration avec Thierry Coquand, Gérard Huet définit le Calcul des Constructions (formalisme fondateur d'une famille de calculs logiques puissants), qui permet d'exprimer avec concision des preuves mathématiques.

 Années 90 :  Conjointement avec Christine Paulin-Mohring, il dirige le projet Coq, qui a mis au point l'assistant de preuves éponyme. C’est l'un des systèmes de développement de mathématiques formelles et de logiciels certifiés les plus utilisés à ce jour.

Mots-clés : Prix EATCS Award Gérard Huet

Haut de page

Suivez Inria