| Naștere |
7 iulie 1947 Bourges |
|---|---|
| Naţionalitate | limba franceza |
| Instruire |
Facultatea de Științe din Paris Școala Națională de Aeronautică și Spațiu ( ro ) Case Western Reserve University Universitatea Paris-Diderot ( doctorat ) (până1976) |
| Activități | Informatician , inginer , logician , profesor universitar |
| Lucrat pentru | Université Paris-Sud , Université Paris-Diderot |
|---|---|
| Camp | Informatică |
| Membru al |
Academia de Științe Academia Europaea (1989) |
| Maestru | George Ernst ( d ) |
| Supervizor | Maurice Nivat |
| Premii |
Gérard Huet (născut la7 iulie 1947în Bourges ) este logician și cercetător în informatică teoretică franceză . Este membru al Academiei de Științe a Institutului Franței , la secțiunea Științe mecanice și computerizate.
Este director de cercetare emerită (de clasă excepțională ) la Institutul Național de Cercetare în Informatică și Automatizare (Inria) și membru al Academiei de Științe . El a fost distins cu premiul Asociației Europene pentru Informatică Teoretică în 2009 și a fost primul beneficiar al Marelui Premiu Inria în 2011.
El este, de asemenea, autorul unui dicționar online sanscrită - franceză , The Sanskrit Heritage Dictionary .
Gérard Huet și-a obținut diploma în inginerie civilă în aeronautică și spațiu (Sup'Aéro) în 1969, în același timp cu un master în informatică de la Facultatea de Științe din Paris . După ce s-a mutat în Statele Unite pentru a se specializa în inteligență artificială, a obținut o diplomă de masterat în 1970 și un doctorat în informatică în 1972 de la Case Western Reserve University din Cleveland . Stăpânul său a fost pe realizarea unui demonstrator interactiv pentru logica 1 st ordine cu egalitate. Doctoratul său a definit o procedură completă de semi-decizie pentru logica de ordin superior (teoria tipului Bisericii), în care căutarea dovezilor este ghidată de un calcul al constrângerilor unificatoare. El a stabilit indecidibilitatea unificării ordinii 3 și un algoritm de semi-unificare în calculul lambda tastat care îi poartă numele.
Revenit în Franța în 1972, a obținut o poziție de cercetare la IRIA ( Institutul de Cercetare în Informatică și Automatizare ) din Rocquencourt . A lucrat acolo cu Gilles Kahn la proiectarea și producția editorului structurat Mentor din 1974 până în 1978. În 1976 a obținut doctoratul în matematică la Universitatea Paris-Diderot . Teza sa a fost despre algoritmul unificării, un proces fundamental al logicii matematice. Apoi și-a îndreptat cercetările către logica egalității și a sistemelor de rescriere cu Jean-Marie Hullot , care a dat naștere sistemului KB de rescriere canonică. Invitat la Stanford Research Institute în 1979-1980, a scris împreună cu Derek Oppen monografia Ecuații și reguli de rescriere . Cu Jean-Jacques Lévy, el a lansat noțiunea unui sistem de rescriere puternic secvențial.
Înapoi la IRIA (care urma să devină INRIA, Institutul Național de Cercetare în Informatică și Automatizare ), a început echipa de proiect Formel în 1982 împreună cu colegul său de la Universitatea Paris-Diderot Guy Cousineau , în colaborare cu laboratorul de informatică al ENS. Acest efort a dat naștere limbajului de programare funcțional Caml , care va fi ulterior reproiectat de Xavier Leroy ca Caml-light apoi OCaml . În 1984-1985 a lucrat cu Thierry Coquand la concepția Calcul des constructions, un sistem logic bazat pe un lambda-calcul tipat cu tipuri dependente, în spiritul limbajului Automath al lui Nicolas de Bruijn. Thierry Coquand a demonstrat în teza sa coerența calculului, în timp ce Gérard Huet a pus împreună cu Motorul constructiv bazele unei mecanizări a calculului, strămoș al sistemului Coq .
Profesor invitat la Universitatea Carnegie Mellon din Pittsburgh în 1985-1986, a predat cursul „ Structuri formale pentru calcul și deducere ”, care va inspira ulterior conferința FSCD. În 1988 a început echipa de proiect Coq cu Christine Paulin-Mohring de la Parallelism Computer Laboratory de la École normale supérieure de Lyon . Acest efort a dat naștere asistentului de probă Coq.
În anii 1990, Gérard Huet a lucrat la diverse probleme de logică matematică și informatică teoretică, în timp ce conducea efortul Coq. El a inventat structura de date Zipper în 1996.
Din 1997 până în 2000, a preluat responsabilitatea de delegat pentru Relații Internaționale la INRIA.
Din 2000 s-a dedicat tratamentului limbajului natural și, în special, al sanscritului . El este autorul primului dicționar de hipertext sanscrit-francez, Dictionnaire Héritage du Sanskrit. El a dezvoltat biblioteca Zen, un set de module OCaml care permit prelucrarea morfo-fonetică a limbajului, folosind automatele decorate oferind o reprezentare eficientă a lexiconelor și traductoarelor raționale. Acest lucru face posibilă în special segmentarea sanscritului prin inversarea sandhi. Această tehnologie a dat naștere noțiunii de Eilenberg Effective Machine, dezvoltată în lucrarea de teză a lui Benoît Razet. Din 2004, site-ul Patrimoniului Sanskrit a furnizat instrumente pentru segmentare, analiză morfologică și gestionarea corpusului sanscrit, în special datorită unei interfețe grafice dezvoltate în colaborare cu Pawan Goyal. Acest software este disponibil pe Gitlab Inria în open source.
Din 2013, Gérard Huet a fost director de cercetare emerit al Inria.
Gérard Huet a fost ales corespondent al Academiei de Științe în 1990, apoi membru în 2002, la secțiunea Științe mecanice și computerizate. Este membru al Academiei Europaea din 1989. Este membru al Comitetului Național Francez pentru Istorie și Filosofie a Științelor.
A primit premiul Herbrand pentru munca sa în Logica Computațională în 1998. Universitatea Chalmers din Göteborg i-a acordat un doctorat Honoris Causa în 2004. A primit premiul EATCS în 2009. În 2011 a fost primul beneficiar al Marelui Premiu Inria. A primit premiul ACM-Sigplan Programming Languages Software și ACM Software System Award în 2013 pentru contribuția sa la asistentul de probă Coq.
Este autorul a numeroase publicații științifice internaționale.