Jo, Gerarde
Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 12. prosince 2016; kontroly vyžadují 17 úprav .| Gerard Hue | |
|---|---|
| Gerard Huet | |
| Datum narození | 7. července 1947 (ve věku 75 let) |
| Místo narození | Bourges |
| Země | |
| Vědecká sféra | Matematika |
| Místo výkonu práce | pařížské univerzitě |
| Alma mater | Case Western Reserve University Paris Diderot University |
| vědecký poradce | Maurice Niva |
| Studenti | Benoît Razet [d] [1] |
| Ocenění a ceny | Cena Evropské asociace pro teoretickou informatiku [d] ( 2009 ) ACM Software System Award [d] ( 2013 ) Herbrand Award [d] ( 1998 ) |
Gérard Pierre Huet ( francouzsky Gérard Huet ) je francouzský vědec v oblasti informatiky, matematiky a lingvistiky. Je hlavním vědeckým ředitelem výzkumu ve společnosti INRIA a je nejlépe známý pro své významné příspěvky k teorii typů , teorii programovacích jazyků a teorii algoritmů .
Životopis
Gerard Huet vystudoval Paris Diderot University (Paříž VII), Case Western Reserve University a University of Paris .
Senior research director ve společnosti INRIA , člen Francouzské akademie věd , člen Evropské akademie . Předtím byl hostujícím profesorem na Asian Institute of Technology v Bangkoku , hostujícím profesorem na Carnegie Mellon University a hostujícím výzkumným pracovníkem na SRI International .
Je autorem sjednocovacího algoritmu pro jednoduše zadaný počet lambda a kompletního důkazu Churchovy metody teorie typů . V letech 1974-1977 pracoval na editoru programu Mentor s Gillesem Kahnem . V letech 1978-1984 pracoval na systému KB rovnicového důkazu spolu s Jean-Marie Hullotem . V 80. letech vedl projekt Formel, který vyvinul programovací jazyk Caml. V roce 1984 vyvinul konstrukční kalkul s Thierrym Cocanem . Vedl projekt Coq v 90. letech s Christine Paulinovou, která vyvinula kontrolu asistenta Coq [2] . Vynalezl datovou strukturu Zipper v roce 1996. V letech 1996-2000 byl vedoucím mezinárodních vztahů ve společnosti INRIA . Vyvinutý soubor nástrojů Zen Computational Linguistics v letech 2000-2004.
Organizoval Institut pro logické základy funkčního programování během Roku programování na University of Texas v Austinu na jaře 1987. Organizoval kolokvium "Testování a zlepšování programů" v Arc et Senans v roce 1975, 5. mezinárodní konferenci o automatizovaném odpočtu (CADE) v Les Arcs v roce 1980, sympozium "Logic in Computer Science" ( The Logic in Computer Science Symposium , LICS) v Paříži v roce 1994 a První mezinárodní sympozium v sanskrtské počítačové lingvistice v roce 2007. Byl koordinátorem ESPRIT European Logic Framework Projects, poté TYPES, od roku 1990 do roku 1995.
Významně přispěl k teorii sjednocení a vývoji typovaných funkcionálních programovacích jazyků, zejména Caml . [3] [4] V poslední době byl odborníkem na počítačovou lingvistiku v sanskrtu . [5] Je správcem webu Sanskrit Heritage Site. [6]
Yue obdržel Herbrand Award v roce 1998 [7] a EATCS Award v roce 2009. [osm]
Publikace
- Le Projet prévision-realisation des vols , Société d'informatique, de conseils et de recherche opérationnelle (SINCRO), Paříž, 1970. WorldCat Record Archived 20. prosince 2016 na Wayback Machine
- Specifikace pour une base commune de données , SINCRO, Paříž, 1971. WorldCat Record Archived 4. dubna 2016 na Wayback Machine
- Gerard P. Huet. Mechanizace teorie typů // Proc. 3rd Int. Společná konf. o umělé inteligenci (IJCAI) (anglicky) / Nils J. Nilsson. - William Kaufmann, 1973. - S. 139-146.
- Gerard P. Huet. Nerozhodnutelnost sjednocení v logice třetího řádu // Informace a kontrola : deník. - 1973. - Sv. 22 . - str. 257-267 . - doi : 10.1016/s0019-9958(73)90301-x .
- La Gestion des données dans les informatiques , École supérieure d'électricité, Malakoff, 1974. WorldCat Record Archived 4. dubna 2016 na Wayback Machine
- "A Unification Algorithm for Typeed Lambda-Calculus" , Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
- Gerard Huet (září 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Université de Paris VII.
- Gerard Huet, Bernard Lang. Prokázání a aplikace transformací programu vyjádřených pomocí vzorů druhého řádu // Acta Informatica : deník. - 1978. - Sv. 11 . - str. 31-55 . - doi : 10.1007/bf00264598 .
- Gerard Huet, DS Lankford. O jednotném problému zastavení pro systémy přepisování termínů . - 1978. - S. 8.
- G. Huet, JM Hullot. Důkazy indukcí v rovnicových teoriích s konstruktory // 21. vyhl. Symp. o základech informatiky . - Ústav elektrických a elektronických inženýrů , 1980. - S. 96-107.
- G. Huet, D.C. Oppen. Rovnice a pravidla přepisování: Průzkum (neurčitý) . - 1980. - S. 52.
- Gerard Huet. Úplný důkaz správnosti Knuth-Bendixova algoritmu dokončení // J. Compput. System Sci. : deník. - 1981. - Sv. 23 . - str. 11-21 . - doi : 10.1016/0022-0000(81)90002-7 .
- Gerard Huet. Formální struktury pro výpočet a dedukce . - 1986. - (Mezinárodní letní škola logiky programování a kalkulací diskrétního designu). Archivováno 14. července 2014 na Wayback Machine
- Gerard Huet. Principy indukce formalizované v počtu konstrukcí / K. Fuchi a M. Nivat. - North-Holland, 1988. - S. 205-216. Archivováno 1. července 2015 na Wayback Machine
- Gerard Huet. Reziduální teorie v λ-kalkulu: formální vývoj . — 1993. Archivováno 1. července 2015 na Wayback Machine
- Huet, GP Design Proof Assistant (vyzvaná přednáška) (Specifikováno) / Ganzinger, Harald. - Springer-Verlag , 1996. - T. 1103. - S. 153. - (LNCS).
- Gerard Huet, H. Laulhere. Konečné převodníky jako regulérní Böhmovy stromy // Teoretické aspekty počítačového softwaru (neopr.) / M. Abadi a T. Ito. - Springer, 1997. - T. 1281. - S. 604-610. — (LNCS). Archivováno 22. prosince 2014 na Wayback Machine
- Gerard Huet. Pravidelné Böhmovy stromy (neurčité) // Math. Struktura. v Comp. Věda. - 1998. - T. 8 . - S. 671-680 . - doi : 10.1017/s0960129598002643 . Archivováno z originálu 24. ledna 2016.
- Gerard Huet. Sjednocení vyššího řádu o 30 let později // Sborník příspěvků, 15. mezinárodní konference TPHOL (anglicky) / V. Carreño a C. Muñoz a S. Tahar. - Springer, 2002. - Sv. 2410. - S. 3-12. — (LNCS). dovětek
- Gerard Huet. Lineární kontexty a funktor sdílení: Techniky pro symbolické výpočty / Fairouz Kamareddine. — Kluwer, 2003. Archivováno 1. července 2015 na Wayback Machine
Poznámky
- ↑ Matematická genealogie (anglicky) - 1997.
- ↑ Co je Coq? | Coq Proof Assistant Archivováno 24. dubna 2016 na Wayback Machine . Coq.inria.fr. Získáno 21. 7. 2013.
- ↑ Pawan Goyal, Gerard Huet. Analýza úplnosti sanskrtského čtenáře // Proceedings of the Fifth International Symposium on Sanskrit Computational Linguistics, Mumbai (anglicky) . - 2013. Archivovaná kopie (nepřístupný odkaz) . Získáno 9. prosince 2016. Archivováno z originálu 14. července 2014.
- ↑ Gerard Huet, Pawan Goyal. Návrh štíhlého rozhraní pro anotaci korpusu v sanskrtu // Proceedings, ICON13, Hyderabad (neopr.) . - 2013. Archivovaná kopie (nepřístupný odkaz) . Získáno 9. prosince 2016. Archivováno z originálu 14. července 2014.
- ↑ Gerard Huet . Archivováno 12. září 2008 na Wayback Machine
- ↑ Místo dědictví sanskrtu . Staženo 9. prosince 2016. Archivováno z originálu 3. června 2013.
- ↑ Herbrandova cena za mimořádný přínos k automatizovanému uvažování (odkaz není k dispozici) . Staženo 9. prosince 2016. Archivováno z originálu 7. února 2015.
- ↑ Cena Evropské asociace pro teoretickou informatiku . Získáno 9. prosince 2016. Archivováno z originálu dne 21. prosince 2016.
Odkazy
- Huet, Gerard (anglicky) v projektu matematické genealogie
- Domovská stránka Gérarda Hueta Archivováno 28. listopadu 2016 na Wayback Machine
- Gérard Huet Héritage du sanskritský slovník sanskrtsko-français . Datum přístupu: 9. prosince 2016. Archivováno z originálu 27. února 2008. (3,32 MB)(428 stran, 5. dubna 2007)
 Tematické stránky | ||||
|---|---|---|---|---|
| ||||