Jo, Gerard
Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 12 december 2016; kontroller kräver 17 redigeringar .| Gerard Huet | |
|---|---|
| Gerard Huet | |
| Födelsedatum | 7 juli 1947 (75 år) |
| Födelseort | Bourges |
| Land | |
| Vetenskaplig sfär | Matte |
| Arbetsplats | universitetet i Paris |
| Alma mater | Case Western Reserve University Paris Diderot University |
| vetenskaplig rådgivare | Maurice Niva |
| Studenter | Benoît Razet [d] [1] |
| Utmärkelser och priser | European Association for Theoretical Computer Science Prize [d] ( 2009 ) ACM Software System Award [d] ( 2013 ) Herbrand Award [d] ( 1998 ) |
Gérard Pierre Huet ( franska Gérard Huet ) är en fransk vetenskapsman inom området datavetenskap, matematik och lingvistik. Han är Chief Scientific Officer of Research vid INRIA och är mest känd för sina betydande bidrag till typteori , programmeringsspråksteori och algoritmteori .
Biografi
Gerard Huet tog examen från Paris Diderot University (Paris VII), Case Western Reserve University och University of Paris .
Senior forskningschef vid INRIA , ledamot av franska vetenskapsakademin , ledamot av Europeiska akademin . Tidigare var han gästprofessor vid Asian Institute of Technology i Bangkok , gästprofessor vid Carnegie Mellon University och gästforskare vid SRI International .
Han är författaren till föreningsalgoritmen för den enkelt skrivna lambdakalkylen och det fullständiga beviset för kyrkans typteorimetod . Han arbetade som redaktör för Mentorprogrammet 1974-1977 tillsammans med Gilles Kahn . 1978-1984 arbetade han på KB:s ekvationsbevissystem tillsammans med Jean-Marie Hullot . Ledde på 1980-talet Formel-projektet som utvecklade programmeringsspråket Caml. 1984 utvecklade han konstruktionskalkylen tillsammans med Thierry Cocan . Ledde Coq- projektet på 1990-talet med Christine Paulin som utvecklade Coq-assistentchecken [2] . Uppfann Zipper- datastrukturen 1996. Han var chef för internationella relationer på INRIA 1996-2000. Utvecklade Zen Computational Linguistics verktygslåda 2000-2004.
Organiserade Institute for Logic Foundations of Functional Programming under programmeringsåret vid University of Texas i Austin våren 1987. Organiserade kollokviet "Program Testing and Improvement" i Arc et Senans 1975, den 5:e internationella konferensen om automatiserat avdrag (CADE) i Les Arcs 1980, symposiet "Logic in Computer Science" ( Logic in Computer Science Symposium , LICS) i Paris 1994 och det första internationella symposiet i Sanskrit Computational Linguistics 2007. Han var koordinator för ESPRIT European Logic Framework Projects, då TYPES, från 1990 till 1995.
Han gjorde stora bidrag till teorin om enande och utvecklingen av maskinskrivna funktionella programmeringsspråk, i synnerhet Caml . [3] [4] Senast var han en beräkningslingvistikforskare på sanskrit . [5] Han är webbansvarig för Sanskrit Heritage Site. [6]
Yue fick Herbrand Award 1998 [7] och EATCS Award 2009. [åtta]
Publikationer
- Le Projet prévision-réalisation des vols , Société d'informatique, de conseils et de recherche opérationnelle (SINCRO), Paris, 1970. WorldCat Record Arkiverad 20 december 2016 på Wayback Machine
- Specifikationer pour une base commune de données , SINCRO, Paris, 1971. WorldCat Record Arkiverad 4 april 2016 på Wayback Machine
- Gerard P. Huet. A Mechanization of Type Theory // Proc. 3:e Int. Gemensam konf. om artificiell intelligens (IJCAI) (engelska) / Nils J. Nilsson. - William Kaufmann, 1973. - S. 139-146.
- Gerard P. Huet. Unifieringens obestämbarhet i tredje ordningens logik // Information och kontroll : journal. - 1973. - Vol. 22 . - s. 257-267 . - doi : 10.1016/s0019-9958(73)90301-x .
- La Gestion des données dans les systèmes informatiques , École supérieure d'électricité, Malakoff, 1974. WorldCat Record Arkiverad 4 april 2016 på Wayback Machine
- "A Unification Algorithm for Typed Lambda-Calculus" , Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
- Gerard Huet (sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Université de Paris VII.
- Gerard Huet, Bernard Lang. Bevisa och tillämpa programtransformationer uttryckta med andra ordningens mönster // Acta Informatica : journal. - 1978. - Vol. 11 . - S. 31-55 . - doi : 10.1007/bf00264598 .
- Gerard Huet, DS Lankford. Om det enhetliga stoppproblemet för termomskrivningssystem . - 1978. - S. 8.
- G. Huet, JM Hullot. Bevis genom induktion i ekvationsteorier med konstruktörer // 21st Ann. Symp. om grunderna för datavetenskap . - Institute of Electrical and Electronics Engineers , 1980. - P. 96-107.
- G. Huet, D.C. Oppen. Ekvationer och omskrivningsregler: En undersökning (obestämd) . - 1980. - S. 52.
- Gerard Huet. Ett fullständigt bevis på riktigheten av Knuth-Bendix-kompletteringsalgoritmen // J. Comput. System Sci. : journal. - 1981. - Vol. 23 . - S. 11-21 . - doi : 10.1016/0022-0000(81)90002-7 .
- Gerard Huet. Formella strukturer för beräkning och avdrag . - 1986. - (International Summer School on Logic of Programming and Calculi of Discrete Design). Arkiverad 14 juli 2014 på Wayback Machine
- Gerard Huet. Induktionsprinciper formaliserade i konstruktionskalkylen / K. Fuchi och M. Nivat. - North-Holland, 1988. - S. 205-216. Arkiverad 1 juli 2015 på Wayback Machine
- Gerard Huet. Residual Theory in λ-Calculus: A formell utveckling . — 1993. Arkiverad 1 juli 2015 på Wayback Machine
- Huet, GP Design Proof Assistant (inbjuden föreläsning) (ospecificerat) / Ganzinger, Harald. - Springer-Verlag , 1996. - T. 1103. - S. 153. - (LNCS).
- Gerard Huet, H. Laulhere. Finita-tillståndsgivare som vanliga Böhm-träd // Teoretiska aspekter av datorprogramvara (neopr.) / M. Abadi och T. Ito. - Springer, 1997. - T. 1281. - S. 604-610. — (LNCS). Arkiverad 22 december 2014 på Wayback Machine
- Gerard Huet. Vanliga Böhm-träd (obestämd) // Matte. Struktur. i Comp. Vetenskap. - 1998. - T. 8 . - S. 671-680 . - doi : 10.1017/s0960129598002643 . Arkiverad från originalet den 24 januari 2016.
- Gerard Huet. Enande av högre ordning 30 år senare // Proceedings, 15th International Conference TPHOL (engelska) / V. Carreño och C. Muñoz och S. Tahar. - Springer, 2002. - Vol. 2410. - S. 3-12. — (LNCS). postskriptum
- Gerard Huet. Linjära sammanhang och delningsfunktionen: Tekniker för symbolisk beräkning / Fairouz Kamareddine. — Kluwer, 2003. Arkiverad 1 juli 2015 på Wayback Machine
Anteckningar
- ↑ Mathematical Genealogy (engelska) - 1997.
- ↑ Vad är Coq? | The Coq Proof Assistant Arkiverad 24 april 2016 på Wayback Machine . Coq.inria.fr. Hämtad 2013-07-21.
- ↑ Pawan Goyal, Gerard Huet. Fullständighetsanalys av en sanskritläsare // Proceedings of the Fifth International Symposium on Sanskrit Computational Linguistics, Mumbai (engelska) . - 2013. Arkiverad kopia (otillgänglig länk) . Hämtad 9 december 2016. Arkiverad från originalet 14 juli 2014.
- ↑ Gerard Huet, Pawan Goyal. Design av ett magert gränssnitt för sanskritkorpusannotering // Proceedings, ICON13, Hyderabad (neopr.) . - 2013. Arkiverad kopia (otillgänglig länk) . Hämtad 9 december 2016. Arkiverad från originalet 14 juli 2014.
- ↑ Gerard Huet . Arkiverad 12 september 2008 på Wayback Machine
- ↑ Sanskrit-arvsplats . Hämtad 9 december 2016. Arkiverad från originalet 3 juni 2013.
- ↑ Herbrand Award för framstående bidrag till automatiserat resonemang (länk ej tillgänglig) . Hämtad 9 december 2016. Arkiverad från originalet 7 februari 2015.
- ↑ European Association for Theoretical Computer Science Award . Hämtad 9 december 2016. Arkiverad från originalet 21 december 2016.
Länkar
- Huet, Gerard (engelska) vid Mathematical Genealogy Project
- Gérard Huets hemsida Arkiverad 28 november 2016 på Wayback Machine
- Gérard Huet Héritage du sanskrit dictionnaire sanskrit-français . Tillträdesdatum: 9 december 2016. Arkiverad från originalet 27 februari 2008. (3,32 MB)(428 sidor, 5 april 2007)
 Tematiska platser | ||||
|---|---|---|---|---|
| ||||