Jo, Gerard
Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 12. december 2016; checks kræver 17 redigeringer .| Gerard Hue | |
|---|---|
| Gerard Huet | |
| Fødselsdato | 7. juli 1947 (75 år) |
| Fødselssted | Bourges |
| Land | |
| Videnskabelig sfære | Matematik |
| Arbejdsplads | Universitetet i Paris |
| Alma Mater | Case Western Reserve University Paris Diderot University |
| videnskabelig rådgiver | Maurice Niva |
| Studerende | Benoît Razet [d] [1] |
| Priser og præmier | European Association for Theoretical Computer Science Prize [d] ( 2009 ) ACM Software System Award [d] ( 2013 ) Herbrand Award [d] ( 1998 ) |
Gérard Pierre Huet ( fransk Gérard Huet ) er en fransk videnskabsmand inden for datalogi, matematik og lingvistik. Han er Chief Scientific Officer of Research ved INRIA og er bedst kendt for sine betydelige bidrag til typeteori , programmeringssprogsteori og algoritmeteori .
Biografi
Gerard Huet er uddannet fra Paris Diderot University (Paris VII), Case Western Reserve University og University of Paris .
Senior forskningsdirektør ved INRIA , medlem af det franske videnskabsakademi , medlem af det europæiske akademi . Tidligere var han gæsteprofessor ved Asian Institute of Technology i Bangkok , gæsteprofessor ved Carnegie Mellon University og gæsteforsker ved SRI International .
Han er forfatteren til foreningsalgoritmen for den enkelt maskinskrevne lambda-regning og det komplette bevis på Churchs typeteoretiske metode . Han arbejdede på redaktøren af Mentor-programmet fra 1974-1977 sammen med Gilles Kahn . I 1978-1984 arbejdede han på KB equational proof system sammen med Jean-Marie Hullot . Ledede i 1980'erne Formel-projektet, som udviklede programmeringssproget Caml. I 1984 udviklede han konstruktionskalkylen sammen med Thierry Cocan . Ledede Coq- projektet i 1990'erne med Christine Paulin, der udviklede Coq-assistenttjekket [2] . Opfandt Zipper -datastrukturen i 1996. Han var chef for internationale relationer hos INRIA fra 1996-2000. Udviklede Zen Computational Linguistics toolkit i 2000-2004.
Organiserede Institute for Logic Foundations of Functional Programming i løbet af programmeringsåret ved University of Texas i Austin i foråret 1987. Arrangerede kollokviet "Program Testing and Improvement" i Arc et Senans i 1975, den 5. internationale konference om automatiseret deduktion (CADE) i Les Arcs i 1980, symposiet "Logic in Computer Science" (logik i computervidenskabssymposium) , LICS) i Paris i 1994 og det første internationale symposium i Sanskrit Computational Linguistics i 2007. Han var koordinator for ESPRIT European Logic Framework Projects, dengang TYPES, fra 1990 til 1995.
Han ydede store bidrag til teorien om forening og udviklingen af maskinskrevne funktionelle programmeringssprog, især Caml . [3] [4] Senest var han en computerlingvistikforsker på sanskrit . [5] Han er webmaster for Sanskrit Heritage Site. [6]
Yue modtog Herbrand Award i 1998 [7] og EATCS Award i 2009. [otte]
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 Arkiveret 20. december 2016 på Wayback Machine
- Specifikationer pour une base commune de données , SINCRO, Paris, 1971. WorldCat Record Arkiveret 4. april 2016 på Wayback Machine
- Gerard P. Huet. En mekanisering af typeteori // Proc. 3. Int. Fælles konf. om kunstig intelligens (IJCAI) (engelsk) / Nils J. Nilsson. - William Kaufmann, 1973. - S. 139-146.
- Gerard P. Huet. Uafgøreligheden ved forening i tredje ordens logik // Information og kontrol : journal. - 1973. - Bd. 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 Arkiveret 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. Bekræftelse og anvendelse af programtransformationer udtrykt med andenordens mønstre // Acta Informatica : journal. - 1978. - Bd. 11 . - S. 31-55 . - doi : 10.1007/bf00264598 .
- Gerard Huet, DS Lankford. Om det ensartede stopproblem for termomskrivningssystemer . - 1978. - S. 8.
- G. Huet, JM Hullot. Beviser ved induktion i ligningsteorier med konstruktører // 21st Ann. Symp. om Datalogiens Grundlag . - Institut for Elektro- og Elektronikingeniører , 1980. - S. 96-107.
- G. Huet, D.C. Oppen. Ligninger og omskrivningsregler: En undersøgelse (ubestemt) . - 1980. - S. 52.
- Gerard Huet. Et fuldstændigt bevis på rigtigheden af Knuth-Bendix fuldførelsesalgoritmen // J. Comput. System Sci. : journal. - 1981. - Bd. 23 . - S. 11-21 . - doi : 10.1016/0022-0000(81)90002-7 .
- Gerard Huet. Formelle strukturer for beregning og fradrag . - 1986. - (International Summer School on Logic of Programming and Calculi of Discrete Design). Arkiveret 14. juli 2014 på Wayback Machine
- Gerard Huet. Induktionsprincipper formaliseret i konstruktionsregningen / K. Fuchi og M. Nivat. - Nord-Holland, 1988. - S. 205-216. Arkiveret 1. juli 2015 på Wayback Machine
- Gerard Huet. Residual Theory in λ-Calculus: A Formal Development . - 1993. Arkiveret 1. juli 2015 på Wayback Machine
- Huet, GP Design Proof Assistant (inviteret foredrag) (uspecificeret) / Ganzinger, Harald. - Springer-Verlag , 1996. - T. 1103. - S. 153. - (LNCS).
- Gerard Huet, H. Laulhere. Finite-state transducere som regulære Böhm-træer // Teoretiske aspekter af computersoftware (neopr.) / M. Abadi og T. Ito. - Springer, 1997. - T. 1281. - S. 604-610. — (LNCS). Arkiveret 22. december 2014 på Wayback Machine
- Gerard Huet. Almindelige Böhm-træer (ubestemt) // Matematik. Struktur. i komp. Videnskab. - 1998. - T. 8 . - S. 671-680 . - doi : 10.1017/s0960129598002643 . Arkiveret fra originalen den 24. januar 2016.
- Gerard Huet. Higher Order Unification 30 år senere // Proceedings, 15th International Conference TPHOL (engelsk) / V. Carreño og C. Muñoz og S. Tahar. - Springer, 2002. - Vol. 2410. - S. 3-12. — (LNCS). efterskrift
- Gerard Huet. Lineære kontekster og delingsfunktionen: Teknikker til symbolsk beregning / Fairouz Kamareddine. — Kluwer, 2003. Arkiveret 1. juli 2015 på Wayback Machine
Noter
- ↑ Matematisk genealogi (engelsk) - 1997.
- ↑ Hvad er Coq? | Coq Proof Assistant arkiveret 24. april 2016 på Wayback Machine . Coq.inria.fr. Hentet 2013-07-21.
- ↑ Pawan Goyal, Gerard Huet. Fuldstændighedsanalyse af en sanskritlæser // Proceedings of the Fifth International Symposium on Sanskrit Computational Linguistics, Mumbai (engelsk) . - 2013. Arkiveret kopi (utilgængeligt link) . Hentet 9. december 2016. Arkiveret fra originalen 14. juli 2014.
- ↑ Gerard Huet, Pawan Goyal. Design af en slank grænseflade til sanskrit -korpusannotering // Proceedings, ICON13, Hyderabad (neopr.) . - 2013. Arkiveret kopi (utilgængeligt link) . Hentet 9. december 2016. Arkiveret fra originalen 14. juli 2014.
- ↑ Gerard Huet . Arkiveret 12. september 2008 på Wayback Machine
- ↑ Sanskrit kulturarvssted . Hentet 9. december 2016. Arkiveret fra originalen 3. juni 2013.
- ↑ Herbrand Award for Distinguished Contributions to Automated Reasoning (link ikke tilgængeligt) . Hentet 9. december 2016. Arkiveret fra originalen 7. februar 2015.
- ↑ European Association for Theoretical Computer Science Award . Hentet 9. december 2016. Arkiveret fra originalen 21. december 2016.
Links
- Huet, Gerard (engelsk) ved Mathematical Genealogy Project
- Gérard Huets hjemmeside Arkiveret 28. november 2016 på Wayback Machine
- Gérard Huet Héritage du sanskrit dictionnaire sanskrit-français . Dato for adgang: 9. december 2016. Arkiveret fra originalen 27. februar 2008. (3,32 MB)(428 sider, 5. april 2007)
 Tematiske steder | ||||
|---|---|---|---|---|
| ||||