|
|
Directeur
de recherche à l'INRIA
Gérard
Huet, né en 1947, docteur ès sciences (1976), est
directeur de recherche à l'Institut national de recherche
en informatique et automatique (INRIA).
Gérard Huet a fait progresser l'informatique
sur le plan conceptuel et a participé à d'importantes
réalisations logicielles.
Spécialiste de démonstration automatique, il a fait
plusieurs contributions aux fondements théoriques de cette
discipline, notamment dans les domaines de logique d'ordre supérieur,
de la logique équationnelle et de la théorie des types.
Il a montré comment l'algorithme d'unification de Herbrand-Robinson
pouvait s'étendre au lambda-calcul typé, permettant
la mécanisation de la théorie des types de Church,
et l'extension du langage PROLOG à la logique d'ordre supérieur.
Il s'est intéressé ensuite à l'automatisation
des raisonnements équationnels par réécriture
canonique, ainsi qu'à l'implémentation efficace de
programmes équationnels séquentiels. Les travaux de
Gérard Huet, obtenus en collaboration avec Jean-Marie Hullot
et Jean-Jacques Levy, sont à la source de l'école
française de réécriture.
Au milieu des années 80, Gérard Huet a travaillé
à la définition d'une théorie des types, le
calcul des constructions, dont le grand pouvoir d'expression permet
de représenter des raisonnements mathématiques sophistiqués,
mais aussi d'exprimer les spécifications d'algorithmes informatiques.
Les preuves formelles de réalisabilité de ces spécifications
sont compilables en un programme exécutable, ouvrant la voie
d'une méthodologie rigoureuse de conception de logiciels
certifiés. Le système d'assistance à la preuve
Coq issu de ces travaux a donné lieu à de nombreuses
collaborations industrielles, notamment avec les sociétés
Dassault Aviation, Bull, France Télécom et Trusted
Logic.
En parallèle avec ces travaux de nature fondamentale, Gérard
Huet a poursuivi des recherches d'un caractère plus appliqué.
En collaboration avec Gilles Kahn, il a participé à
la conception et à la réalisation d'un éditeur
de structures hiérarchiques appelé Mentor. Ces travaux,
précurseurs sur la syntaxe abstraite, ont ouvert la voie
à des environnements de programmation, tels que Centaur,
et à des formats d'échange structurés tels
que XML.
Dans les années 80, Gérard Huet a dirigé le
projet Formel, dont le but était de définir et d'implémenter
des systèmes de manipulation d'objets mathématiques,
et de les appliquer aux outils de base du génie logiciel.
Reprenant comme langage de programmation le langage ML, il a dirigé
l'effort de conception et d'implémentation d'un langage fonctionnel
puissant appelé CAML. L'environnement de programmation "Objective
CAML" est utilisé par une large communauté pour
l'enseignement de la programmation et l'implémentation de
logiciels sûrs.
Depuis quelques années, Gérard Huet s'est tourné
vers la modélisation mathématique et informatique
des langues, et développe des outils efficaces de linguistique
computationnelle. Il est l'auteur d'une bibliothèque de transducteurs d'état fini "Zen", permettant d'exprimer et de résoudre des tâches de représentation de lexiques, de calculs morpho-phonémiques, de segmentation et d'analyse syntaxico-sémantique superficielle. Il a mis en œuvre ces techniques dans une plate-forme d'analyse informatique du sanskrit permettant l'étiquetage automatique de phrases du sanskrit classique, et indexant un dictionnaire hypertexte sanskrit-français original. Ce logiciel est disponible comme ensemble de services Web à l'URL "http://sanskrit.inria.fr".
Mots
clés : démonstration automatique, théorie des
types, unification, lambda-calcul, logique constructive, programmation
fonctionnelle, linguistique computationnelle
Prix et distinctions
Membre de l'Academia Europaea (1989)
Prix Herbrand de la "Conference on automated deduction"
(1998)
Doctorat Honoris Causa de l'Université Chalmers à Göteborg (2004)
EATCS Award de l'European Association for Theoretical Computer Science (2009)
Publications
les plus représentatives
G. HUET
A unification algorithm for typed lambda-calculus
Journal of Theoretical Computer Science, (1975) 1, 27-58
G. HUET
Confluent reductions : abstract properties and applications to term rewriting systems
JACM (1980) 27, 797-821
T. COQUAND, G. HUET
The calculus of constructions
Information and Computation (1988) 76, 95-120
G. HUET
The constructive engine
Invited Conference, 2nd European Symposium on Programming, Nancy,
(1988). In "Theoretical Computer Science", in memory
of Gift Siromoney, Ed. R. NARASIMHAN, World Scientific Publishing
(1989)
G. HUET, J.J. LÉVY
Call by need computations in orthogonal term rewriting systems
In Computational Logic, J.A. Robinson anniversary volume, Eds
J. L. LASSEZ and G. PLOTKIN, MIT Press, 1991
G. HUET
An analysis of Böhm's theorem
Theoretical Computer Science (1993) 121, 145-167
G. HUET
Residual theory in lambda-calculus : A formal development
J. Functional Programming (1994) 4, 371-394
G. HUET
The Zipper
J. Functional Programming (1997) 7, 549-554
G. HUET, A. SAÏBI
Constructive Category Theory
CLICS-TYPES BRA meeting, 1995 In "Proof, language and interaction
- Essays in honour of Robin Milner". Eds. G. PLOTKIN, C.
STIRLING, M. TOFTE, MIT Press (2000)
G. HUET
A Functional Toolkit for Morphological and Phonological Processing,
Application to a Sanskrit Tagger.
Journal of Functional Programming 15 (4) pp. 573-614 (2005)
G. HUET
Lexicon-directed Segmentation and Tagging of Sanskrit.
In "Themes and Tasks in Old and Middle Indo-Aryan Linguistics"
Eds. Bertil Tikkanen & Heinrich Hettrich. Motilal Banarsidass, Delhi, pp.
307-325 (2006)
Principaux
ouvrages
G. HUET (Editor)
Logical foundations of functional programming
Addison-Wesley (1990)
G. HUET, G. PLOTKIN, eds.
Logical frameworks
Cambridge University Press (1991)
G. HUET, G. PLOTKIN, eds.
Logical environments
Cambridge University Press (1993)
G. HUET, A. KULKARNI & P. SCHARF, Eds.
Sanskrit Computational Linguistics 1 and 2
Ed. Springer-Verlag Lecture Notes 5402 (2009)
G. HUET & A. KULKARNI, Eds.
Sanskrit Computational Linguistics 3.
Springer-Verlag Lecture Notes 5406 (2009)
Y. BERTOT, G. HUET, J.J. LÉVY & G. PLOTKIN, Eds.
From Semantics to Computer Science - Essays in Honour of Gilles Kahn.
Ed. Cambridge University Press (2009)
Le
18 mai 2009
|
