Da, Gerard

Gérard Pierre Huet ( franceză  Gérard Huet ) este un om de știință francez în domeniul informaticii, matematicii și lingvisticii. El este directorul științific al cercetării la INRIA și este cel mai bine cunoscut pentru contribuțiile sale semnificative la teoria tipurilor , teoria limbajului de programare și teoria algoritmilor .

Biografie

Gerard Huet a absolvit Universitatea Paris Diderot (Paris VII), Universitatea Case Western Reserve și Universitatea din Paris .

Director senior de cercetare la INRIA , membru al Academiei Franceze de Științe , membru al Academiei Europene . Anterior, a fost profesor invitat la Institutul Asiatic de Tehnologie din Bangkok , profesor invitat la Universitatea Carnegie Mellon și cercetător invitat la SRI International .

El este autorul algoritmului de unificare pentru calculul lambda tip simplu și dovada completă a metodei teoriei tipurilor a lui Church . A lucrat la editorul programului Mentor din 1974-1977 cu Gilles Kahn . În 1978-1984 a lucrat la sistemul de demonstrare ecuațională KB împreună cu Jean-Marie Hullot . A condus proiectul Formel în anii 1980, care a dezvoltat limbajul de programare Caml. În 1984 a dezvoltat calculul de construcție cu Thierry Cocan . A condus proiectul Coq în anii 1990, împreună cu Christine Paulin, dezvoltând verificarea asistentului Coq [2] . A inventat structura de date Zipper în 1996. A fost șeful de relații internaționale la INRIA între 1996-2000. A dezvoltat set de instrumente Zen Computational Linguistics în 2000-2004.

A organizat Institutul pentru Fundamentele Logice de Programare Funcțională în timpul Anului Programării de la Universitatea Texas din Austin în primăvara anului 1987. A organizat colocviul „Program Testing and Improvement” la Arc et Senans în 1975, a 5-a Conferință Internațională de Deducere Automatizată (CADE) în Les Arcs în 1980, simpozionul „Logic in Computer Science” ( The Logic in Computer Science Symposium) , LICS) la Paris în 1994 și primul simpozion internațional de lingvistică computațională sanscrită în 2007. A fost coordonator al proiectelor-cadru logice europene ESPRIT, apoi TYPES, din 1990 până în 1995.

El a adus contribuții majore la teoria unificării și dezvoltarea limbajelor de programare funcționale tipizate, în special Caml . [3] [4] Cel mai recent a fost un savant în lingvistică computațională în sanscrită . [5] El este webmasterul site-ului patrimoniului sanscrit. [6]

Yue a primit premiul Herbrand în 1998 [7] și premiul EATCS în 2009. [opt]

Publicații

• Le Projet prévision-réalisation des vols , Société d'informatique, de conseils et de recherche opérationnelle (SINCRO), Paris, 1970. WorldCat Record Arhivat la 20 decembrie 2016 la Wayback Machine
• Spécifications pour une base commune de données , SINCRO, Paris, 1971. WorldCat Record Arhivat la 4 aprilie 2016 la Wayback Machine
• Gerard P. Huet. O mecanizare a teoriei tipurilor // Proc. al 3-lea int. Conf. comună. on Artificial Intelligence (IJCAI)  (engleză) / Nils J. Nilsson. - William Kaufmann, 1973. - P. 139-146.
• Gerard P. Huet.  Indecidibilitatea unificării în logica de ordin al treilea  // Informare și control : jurnal. - 1973. - Vol. 22 . - P. 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 Arhivat la 4 aprilie 2016 la Wayback Machine
• „A Unification Algorithm for Typed Lambda-Calculus” , Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
• Gerard Huet (sept 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universitatea din Paris VII.
• Gerard Huet, Bernard Lang. Demonstrarea și aplicarea transformărilor de program exprimate cu modele de ordinul doi  //  Acta Informatica : jurnal. - 1978. - Vol. 11 . - P. 31-55 . - doi : 10.1007/bf00264598 .
• Gerard Huet, DS Lankford. Despre problema de oprire uniformă pentru sistemele de rescriere a termenilor  . - 1978. - P. 8.

• G. Huet, JM Hullot. Demonstrații prin inducție în teorii ecuaționale cu constructori // 21st Ann. Symp.  pe Fundamentele Informaticii . - Institutul de Ingineri Electricieni şi Electronici , 1980. - P. 96-107.
• G. Huet, D.C. Oppen. Ecuații și reguli de rescrie: un sondaj  (nedefinit) . - 1980. - S. 52.
• Gerard Huet. O dovadă completă a corectitudinii algoritmului de completare Knuth-Bendix  //  J. Comput. Sistem Sci. : jurnal. - 1981. - Vol. 23 . - P. 11-21 . - doi : 10.1016/0022-0000(81)90002-7 .
• Gerard Huet. Structuri formale pentru calcul și  deducție . - 1986. - (Școala Internațională de Vară de Logica de Programare și Calcule de Design Discret). Arhivat pe 14 iulie 2014 la Wayback Machine
• Gerard Huet. Principii de inducție formalizate în calculul construcțiilor  / K. Fuchi și M. Nivat. - Olanda de Nord, 1988. - P. 205-216. Arhivat la 1 iulie 2015 la Wayback Machine

• Gerard Huet. Teoria reziduală în λ-Calcul: O  dezvoltare formală . — 1993. Arhivat la 1 iulie 2015 la Wayback Machine
• Huet, GP Design Proof Assistant (prelegere invitată)  (nespecificat) / Ganzinger, Harald. - Springer-Verlag , 1996. - T. 1103. - S. 153. - (LNCS).
• Gerard Huet, H. Laulhere. Transductori cu stări finite ca arbori Böhm obișnuiți // Aspecte teoretice ale software-ului de calculator  (neopr.) / M. Abadi și T. Ito. - Springer, 1997. - T. 1281. - S. 604-610. — (LNCS). Arhivat pe 22 decembrie 2014 la Wayback Machine
• Gerard Huet. Arbori Böhm obișnuiți  (nedefiniti)  // Matematică. Struct. în Comp. Ştiinţă. - 1998. - T. 8 . - S. 671-680 . - doi : 10.1017/s0960129598002643 . Arhivat din original pe 24 ianuarie 2016.

• Gerard Huet. Higher Order Unification 30 years later // Proceedings, a 15th International Conference TPHOL  (engleză) / V. Carreño and C. Muñoz and S. Tahar. - Springer, 2002. - Vol. 2410. - P. 3-12. — (LNCS). postscriptum
• Gerard Huet. Contexte liniare și funcția de partajare: tehnici de calcul simbolic  / Fairouz Kamareddine. — Kluwer, 2003. Arhivat la 1 iulie 2015 la Wayback Machine

Note

1. ↑ Genealogia matematică  (engleză) - 1997.
2. ↑ Ce este Coq? | The Coq Proof Assistant Arhivat 24 aprilie 2016 la Wayback Machine . Coq.inria.fr. Preluat la 21.07.2013.
3. ↑ Pawan Goyal, Gerard Huet. Analiza completă a unui cititor de sanscrită // Proceedings of the Fifth International Symposium on Sanskrit Computational Linguistics, Mumbai  (engleză) . - 2013. Copie arhivată (link inaccesibil) . Preluat la 9 decembrie 2016. Arhivat din original la 14 iulie 2014. (nedefinit) 
4. ↑ Gerard Huet, Pawan Goyal. Design of a lean interface for sanscrită corpus adnotation // Proceedings, ICON13, Hyderabad  (neopr.) . - 2013. Copie arhivată (link inaccesibil) . Preluat la 9 decembrie 2016. Arhivat din original la 14 iulie 2014. (nedefinit) 
5. ↑ Gerard Huet . Arhivat pe 12 septembrie 2008 la Wayback Machine
6. ↑ Situl de patrimoniu sanscrit . Consultat la 9 decembrie 2016. Arhivat din original pe 3 iunie 2013. (nedefinit)
7. ↑ Premiul Herbrand pentru contribuții distinse la raționamentul automatizat (link nu este disponibil) . Consultat la 9 decembrie 2016. Arhivat din original pe 7 februarie 2015. (nedefinit) 
8. ↑ Premiul Asociației Europene pentru Informatică Teoretică . Preluat la 9 decembrie 2016. Arhivat din original la 21 decembrie 2016. (nedefinit)

Link -uri

• Huet, Gerard  (engleză) la proiectul de genealogie matematică
• Pagina de pornire a lui Gérard Huet Arhivată 28 noiembrie 2016 la Wayback Machine
• Gérard Huet Héritage du sanscrit dictionnaire sanscrit-français . Data accesului: 9 decembrie 2016. Arhivat din original la 27 februarie 2008.  (nedefinit)  (3,32 MB)(428 de pagini, 5 aprilie 2007)

Site-uri tematice	Google Academic Genealogie matematică zbMATH Deschide
În cataloagele bibliografice BNF : 11907937c GND : 1079124640 ISNI : 0000 0001 1932 5321 J9U : 987007444796905171 LCCN : n81087432 NKC : xx0233005 NTA : 074993321 NUKAT : n94301441 SUDOC : 026927241 VIAF : 14812854 WorldCat VIAF : 14812854