| Fødsel |
7. juli 1947 Bourges |
|---|---|
| Nasjonalitet | fransk |
| Opplæring |
Paris fakultet for vitenskaper National School of Aeronautics and Space ( en ) Case Western Reserve University Paris-Diderot University ( doktorgrad ) (til1976) |
| Aktiviteter | Informatiker , ingeniør , logiker , universitetsprofessor |
| Jobbet for | Université Paris-Sud , Université Paris-Diderot |
|---|---|
| Felt | Informatikk |
| Medlem av |
Vitenskapsakademiet Academia Europaea (1989) |
| Herre | George Ernst ( d ) |
| Veileder | Maurice Nivat |
| Utmerkelser |
Gérard Huet (født den7. juli 1947i Bourges ) er en logiker og forsker i teoretisk datavitenskap fransk . Han er medlem av Academy of Sciences ved Institut de France , i delen Mechanical and Computer Sciences.
Han er direktør for emeritusforskning (av eksepsjonell klasse ) ved National Institute for Research in Computer Science and Automation (Inria) og medlem av Academy of Sciences . Han ble tildelt European Association for Theoretical Computer Science Prize i 2009 og var den første mottakeren av Inria Grand Prix i 2011.
Han er også forfatter av en online sanskrit - fransk ordbok , The Sanskrit Heritage Dictionary .
Gérard Huet oppnådde sitt diplom i sivilingeniør i luftfart og romfart (Sup'Aéro) i 1969, samtidig som en mastergrad i informatikk fra fakultetet for vitenskap i Paris . Etter å ha flyttet til USA for å spesialisere seg i kunstig intelligens, oppnådde han en mastergrad i 1970 og en doktorgrad i informatikk i 1972 fra Case Western Reserve University i Cleveland . Hans herre var på realisering av en interaktiv demonstrator for logikk 1 st orden med likestilling. Hans doktorgrad definerte en fullstendig semi-beslutningsprosedyre for høyere ordenslogikk (Kirkens typeteori), hvor jakten på bevis styres av en beregning av samlende begrensninger. Han etablerte ubesluttsomheten om forening av ordre 3, og en semi-foreningsalgoritme i den typede lambdakalkulus som bærer navnet hans.
Da han kom tilbake til Frankrike i 1972, fikk han en forskerstilling ved IRIA ( Institute for Research in Computer Science and Automation ) i Rocquencourt . Han jobbet der sammen med Gilles Kahn med design og produksjon av den strukturerte redaktøren Mentor fra 1974 til 1978. I 1976 oppnådde han doktorgrad i matematikk ved University of Paris-Diderot . Avhandlingen hans handlet om algoritmen for forening, en grunnleggende prosess for matematisk logikk. Deretter orienterte han forskningen mot logikken i likhets- og omskrivningssystemer med Jean-Marie Hullot , som ga opphav til KB-systemet for kanonisk omskriving. Invitert til Stanford Research Institute i 1979-1980, skrev han med Derek Oppen monografien Equations and Rewrite rules . Med Jean-Jacques Lévy utgav han forestillingen om et sterkt sekvensielt omskrivingssystem.
Tilbake på IRIA (som skulle bli INRIA, National Institute for Research in Computer Science and Automation ), startet han Formel-prosjektgruppen i 1982 sammen med sin kollega fra Paris-Diderot University Guy Cousineau , i samarbeid med datavitenskapslaboratoriet til ENS. Denne innsatsen fødte det funksjonelle programmeringsspråket Caml , som senere ble redesignet av Xavier Leroy som Caml-light og deretter OCaml . I 1984-1985 jobbet han med Thierry Coquand om oppfatningen av Calcul des konstruksjoner, et logisk system basert på en skrevet lambda-kalkulus med avhengige typer, i ånden til Automath-språket til Nicolas de Bruijn. Thierry Coquand beviste i sin avhandling koherensen i beregningen, mens Gérard Huet stilte med Constructive Engine grunnlaget for en mekanisering av beregningen, forfader til Coq- systemet .
Gjesteprofessor ved Carnegie Mellon University i Pittsburgh i 1985-1986, underviste han i kurset " Formal Structures for Computation and Deduction " som senere skulle inspirere FSCD-konferansen. I 1988 startet han Coq-prosjektgruppen med Christine Paulin-Mohring fra Parallelism Informatics Laboratory ved École normale supérieure de Lyon . Denne innsatsen fødte bevisassistenten Coq.
På 1990-tallet arbeidet Gérard Huet med ulike problemer innen matematisk logikk og teoretisk informatikk, mens han ledet Coq-innsatsen. Han oppfant Zipper-datastrukturen i 1996.
Fra 1997 til 2000 overtok han ansvaret for delegat for internasjonale relasjoner i INRIA.
Siden 2000 har han viet seg til behandling av naturlig språk, og spesielt sanskrit . Han er forfatter av den første sanskrit-franske hypertekstordboken, Dictionnaire Héritage du Sanskrit. Han utviklet Zen-biblioteket, et sett med OCaml-moduler som tillater morfofonetisk behandling av språket, ved hjelp av dekorerte automater som gir en effektiv representasjon av leksikoner og rasjonelle svingere. Dette gjør det spesielt mulig å segmentere sanskrit ved inversjon av sandhi. Denne teknologien fødte forestillingen om Eilenberg Effective Machine, utviklet i avhandlingen til Benoît Razet. Siden 2004 har Sanskrit Heritage-området gitt verktøy for segmentering, morfologisk analyse og styring av Sanskrit corpus, særlig takket være et grafisk grensesnitt utviklet i samarbeid med Pawan Goyal. Denne programvaren er tilgjengelig på Gitlab Inria i åpen kildekode.
Siden 2013 har Gérard Huet vært emeritus-forskningsdirektør i Inria.
Gérard Huet ble valgt til korrespondent for vitenskapsakademiet i 1990, deretter medlem i 2002, i seksjonen Mekanisk og informatikk. Han har vært medlem av Academia Europaea siden 1989. Han er medlem av den franske nasjonale komiteen for vitenskapens historie og filosofi.
Han mottok Herbrand-prisen for sitt arbeid i Computational Logic i 1998. Chalmers University i Göteborg tildelte ham en Honoris Causa-doktorgrad i 2004. Han mottok EATCS-prisen i 2009. I 2011 var han den første mottakeren av Inria Grand Prix. Han mottok ACM-Sigplan Programming Languages Software Award og ACM Software System Award i 2013 for sitt bidrag til Coq proof assistent.
Han er forfatter av en rekke internasjonale vitenskapelige publikasjoner.