| Narození |
July 7 , v roce 1947 Bourges |
|---|---|
| Státní příslušnost | francouzština |
| Výcvik |
Pařížská Přírodovědecká fakulta Národní škola letectví a kosmonautiky ( en ) Univerzita Case Western Reserve University Paris-Diderot University ( doktorát ) (do1976) |
| Činnosti | Počítačový vědec , inženýr , logik , univerzitní profesor |
| Pracoval pro | Université Paris-Sud , Université Paris-Diderot |
|---|---|
| Pole | Počítačová věda |
| Člen |
Akademie věd Academia Europaea (1989) |
| Mistr | George Ernst ( d ) |
| Dozorce | Maurice Nivat |
| Ocenění |
Gérard Huet (narozen dne7. července 1947v Bourges ) je logik a výzkumný pracovník v oblasti teoretické informatiky ve francouzštině . Je členem Akademie věd v Institut de France , v úseku strojní a počítačové vědy.
Je ředitelem emeritního výzkumu ( výjimečné třídy ) v Národním ústavu pro výzkum v informatice a automatizaci (Inria) a členem Akademie věd . V roce 2009 mu byla udělena cena Evropské asociace pro teoretickou informatiku a v roce 2011 byl prvním příjemcem Inria Grand Prix.
Je také autorem online slovníku sanskrt - francouzština , The Sanskrit Heritage Dictionary .
Gérard Huet získal diplom ze stavebního inženýrství v letectví a kosmonautice (Sup'Aéro) v roce 1969, současně jako magisterský titul v oboru počítačových věd na pařížské Přírodovědecké fakultě . Po přestěhování do Spojených států se specializací na umělou inteligenci získal v roce 1970 magisterský titul a v roce 1972 titul Ph.D. v oboru počítačových věd na Case Western Reserve University v Clevelandu . Jeho pán byl na realizaci interaktivního demonstrátoru pro logiku 1 prvním pořadí se rovnosti. Jeho Ph.D. definoval kompletní semi-rozhodovací postup pro logiku vyššího řádu (církevní teorie typů), kde se hledání důkazů řídí výpočtem sjednocujících omezení. Stanovil nerozhodnutelnost sjednocení řádu 3 a semi-algoritmus sjednocení v zadaném lambda-kalkulu, který nese jeho jméno.
Po návratu do Francie v roce 1972 získal výzkumnou pozici na IRIA ( Institute for Research in Computer Science and Automation ) v Rocquencourt . Pracoval tam s Gillesem Kahnem na návrhu a výrobě strukturovaného editora Mentora v letech 1974 až 1978. V roce 1976 získal doktorát z matematiky na univerzitě v Paříži - Diderot . Jeho práce byla o algoritmu sjednocení, základním procesu matematické logiky. Svůj výzkum poté zaměřil na logiku systémů rovnosti a přepisování s Jean-Marie Hullotem , který dal vzniknout systému kanonického přepisování KB. V letech 1979–1980 byl pozván do Stanfordského výzkumného ústavu a spolu s Derekem Oppenem napsal monografii Rovnice a pravidla přepisování . S Jean-Jacquesem Lévym vydal pojem silně sekvenčního přepisovacího systému.
V IRIA (která se měla stát INRIA, Národním ústavem pro výzkum v oblasti výpočetní techniky a automatizace ) zahájil v roce 1982 projektový tým společnosti Formel se svým kolegou z univerzity Paris-Diderot Guy Cousineau ve spolupráci s laboratoří výpočetní techniky ENS. Toto úsilí dalo vzniknout funkčnímu programovacímu jazyku Caml , který byl později přepracován Xavierem Leroyem jako Caml-light pak OCaml . V letech 1984-1985 pracoval s Thierrym Coquandem na koncepci Calcul des konstrukcí, logického systému založeného na zadaném lambda-kalkulu se závislými typy, v duchu jazyka Automath od Nicolase de Bruijn. Thierry Coquand ve své práci prokázal soudržnost výpočtu, zatímco Gérard Huet představoval s konstruktivním motorem základy mechanizace výpočtu, předchůdce systému Coq .
Hostující profesor na Carnegie Mellon University v Pittsburghu v letech 1985–1986 vyučoval kurz „ Formální struktury pro výpočet a odvod“, který by později inspiroval konferenci FSCD. V roce 1988 zahájil projektový tým Coq s Christine Paulin-Mohringovou z počítačové laboratoře paralelismu École normale supérieure de Lyon . Z tohoto úsilí se zrodil asistent kontroly Coq.
V 90. letech pracoval Gérard Huet na různých problémech matematické logiky a teoretické informatiky, přičemž vedl úsilí Coq. V roce 1996 vynalezl datovou strukturu Zipper.
V letech 1997 až 2000 převzal odpovědnost delegáta pro mezinárodní vztahy ve společnosti INRIA.
Od roku 2000 se věnuje léčbě přirozeného jazyka, zejména sanskrtu . Je autorem prvního sanskritsko-francouzského hypertextového slovníku, Slovníku Héritage du Sanskrit. Vyvinul knihovnu Zen, sadu modulů OCaml umožňujících morfofonické zpracování jazyka, pomocí zdobených automatů poskytujících efektivní reprezentaci lexikonů a racionálních převodníků. To umožňuje zejména segmentovat sanskrt inverzí sandhi. Tato technologie dala vzniknout pojmu Eilenberg Effective Machine, který byl vyvinut v diplomové práci Benoîta Razeta. Od roku 2004 poskytuje stránka sanskrtského dědictví nástroje pro segmentaci, morfologickou analýzu a správu sanskrtského korpusu, zejména díky grafickému rozhraní vyvinutému ve spolupráci se společností Pawan Goyal. Tento software je k dispozici na Gitlab Inria v otevřeném zdroji.
Od roku 2013 je Gérard Huet emeritním výzkumným ředitelem Inria.
Gérard Huet byl zvolen za korespondenta Akademie věd v roce 1990, poté členem v roce 2002, v sekci Mechanické a počítačové vědy. Od roku 1989 je členem Academia Europaea . Je členem francouzského Národního výboru pro dějiny a filozofii věd.
V roce 1998 získal Herbrandovu cenu za práci ve výpočetní logice. Chalmers University v Göteborgu mu v roce 2004 udělil doktorát Honoris Causa. Cenu EATCS získal v roce 2009. V roce 2011 byl prvním držitelem Grand Prix Inria. V roce 2013 obdržel cenu ACM-Sigplan Programming Languages Software Award a cenu ACM Software System Award za svůj příspěvek asistentovi Coq proof.
Je autorem řady mezinárodních vědeckých publikací.