PROFILPELAJAR.COM

Жерар Юэ
Жерар Юэ
	фр. Gérard Huet
Дата рождения	7 июля 1947 (77 лет)
Место рождения	Бурж
Страна	Франция;
Род деятельности	специалист в области информатики, инженер, логик, преподаватель университета, математик
Научная сфера	Математика
Место работы	Парижский университет
Альма-матер	Университет Кейс Вестерн Резерв Университет Париж Дидро
Научный руководитель	Морис Нива
Ученики	Benoît Razet[вд]
Награды и премии	премия Европейской ассоциации теоретической информатики[вд] (2009) премия ACM по системному программному обеспечению[вд] (2013) Премия Эрбрана[вд] (1998)
Сайт	gallium.inria.fr/~huet/

Жерар Пьер Юэ (фр. Gérard Huet) — французский учёный в области информатики, математики и лингвистики. Является главным научным директором по исследованиям в INRIA и наиболее известен благодаря значительному вкладу в теорию типов, теорию языка программирования и теорию алгоритмов.

Биография

Жерар Юэ окончил университет Париж Дидро (Париж VII), университет Кейс Вестерн Резерв и Парижский университет.

Cтарший директор по исследованиям INRIA, член Французской академии наук, член Европейской Академия. Ранее он был приглашенным профессором в Азиатском технологическом институте в Бангкоке, приглашенным профессором Университета Карнеги-Меллона и приглашенным исследователем в компании SRI International.

Является автором алгоритма унификации^[англ.] для просто типизированного лямбда-исчисления и полного доказательства метод теории типов Чёрча. Он работал над редактором программы Mentor в 1974—1977 годах с Жилем Каном. В 1978—1984 годах работал над КБ эквациональной системой доказательств совместно с Жаном-Мари Юлло. Возглавлял проект Formel в 1980-х годах, который разработал язык программирования Caml. В 1984 году разработал исчисление конструкций совместно с Тьерри Коканом. Возглавлял проект Coq в 1990-х годах с Кристин Полин, разрабатывавшей проверку ассистента Coq^[2]. Изобрел структуру данных Zipper^[англ.] в 1996. Был руководителем международных отношений INRIA в 1996—2000 гг. Разработал Zen Computational Linguistics toolkit в 2000—2004 гг.

Организовал Институт Логических Основ Функционального Программирования в течение Года Программирования в Техасском университете в Остине весной 1987 года. Организовал коллоквиум «Испытание и улучшение программ» в Арк э Сенан^[англ.] в 1975, 5-ю Международную Конференцию по Автоматизированным Вычислениям (International Conference on Automated Deduction, CADE) в Лез-Арк в 1980, симпозиум «Логика в компьютерных науках» (the Logic in Computer Science Symposium, LICS) в Париже в 1994 и Первый международный симпозиум в Санскритской Компьютерной Лингвистике (First International Symposium in Sanskrit Computational Linguistics) в 2007 году. Был координатором ESPRIT Европейских проектов логических фремворков, затем TYPES, с 1990 до 1995.

Он внес большой вклад в теорию объединения и развития типизированных функциональных языков программирования, в частности Caml.^[3]^[4] Совсем недавно он был ученым по компьютерной лингвистике на санскрите.^[5] Является веб-мастером сайта the Sanskrit Heritage Site.^[6]

Юэ получил премию Эрбрана в 1998 году^[7] и премию EATCS в 2009 году.^[8]

Публикации

Le Projet prévision-réalisation des vols, Société d’informatique, de conseils et de recherche opérationnelle (SINCRO), Paris, 1970. WorldCat Record Архивная копия от 20 декабря 2016 на Wayback Machine
Spécifications pour une base commune de données, SINCRO, Paris, 1971. WorldCat Record Архивная копия от 4 апреля 2016 на Wayback Machine
Gérard P. Huet. A Mechanization of Type Theory // Proc. 3rd Int. Joint Conf. on Artificial Intelligence (IJCAI) (англ.) / Nils J. Nilsson. — William Kaufmann, 1973. — P. 139—146.
Gérard P. Huet. The Undecidability of Unification in Third Order Logic (англ.) // Information and Control^[англ.] : journal. — 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 Архивная копия от 4 апреля 2016 на Wayback Machine
«A Unification Algorithm for Typed Lambda-Calculus», Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universite de Paris VII.
Gérard Huet, Bernard Lang. Proving and Applying Program Transformations Expressed with Second-Order Patterns (англ.) // Acta Informatica^[англ.] : journal. — 1978. — Vol. 11. — P. 31—55. — doi:10.1007/bf00264598.
Gérard Huet, D.S. Lankford. On the Uniform Halting Problem for Term Rewriting Systems (англ.). — 1978. — P. 8.

G. Huet, J.M. Hullot. Proofs by Induction in Equational Theories with Constructors // 21st Ann. Symp. on Foundations of Computer Science (англ.). — Institute of Electrical and Electronics Engineers, 1980. — P. 96—107.
G. Huet, D.C. Oppen. Equations and Rewrite Rules: A Survey (неопр.). — 1980. — С. 52.
Gérard Huet. A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm (англ.) // J. Comput. System Sci. : journal. — 1981. — Vol. 23. — P. 11—21. — doi:10.1016/0022-0000(81)90002-7.
Gérard Huet. Formal Structures for Computation and Deduction (англ.). — 1986. — (International Summer School on Logic of Programming and Calculi of Discrete Design). Архивная копия от 14 июля 2014 на Wayback Machine
Gérard Huet. Induction Principles Formalized in the Calculus of Constructions (англ.) / K. Fuchi and M. Nivat. — North-Holland, 1988. — P. 205—216. Архивная копия от 1 июля 2015 на Wayback Machine

Gérard Huet. Residual Theory in λ-Calculus: A Formal Development (англ.). — 1993. Архивная копия от 1 июля 2015 на Wayback Machine
Huet, G.P. Design Proof Assistant (invited lecture) (неопр.) / Ganzinger, Harald. — Springer-Verlag, 1996. — Т. 1103. — С. 153. — (LNCS).
Gérard Huet, H. Laulhère. Finite-state Transducers as Regular Böhm Trees // Theoretical Aspects of Computer Software (неопр.) / M. Abadi and T. Ito. — Springer, 1997. — Т. 1281. — С. 604—610. — (LNCS). Архивная копия от 22 декабря 2014 на Wayback Machine
Gérard Huet. Regular Böhm Trees (неопр.) // Math. Struct. in Comp. Science. — 1998. — Т. 8. — С. 671—680. — doi:10.1017/s0960129598002643. Архивировано 24 января 2016 года.

Gérard Huet. Higher Order Unification 30 years later // Proceedings, 15th International Conference TPHOL (англ.) / V. Carreño and C. Muñoz and S. Tahar. — Springer, 2002. — Vol. 2410. — P. 3—12. — (LNCS). Postscript
Gérard Huet. Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation (англ.) / Fairouz Kamareddine. — Kluwer^[англ.], 2003. Архивная копия от 1 июля 2015 на Wayback Machine

Примечания

↑ Mathematics Genealogy Project (англ.) — 1997.
↑ What is Coq ? | The Coq Proof Assistant Архивная копия от 24 апреля 2016 на Wayback Machine. Coq.inria.fr. Retrieved on 2013-07-21.
↑ Архивированная копия (англ.). Дата обращения: 9 декабря 2016. Архивировано из оригинала 14 июля 2014 года.Архивированная копия (неопр.). Дата обращения: 9 декабря 2016. Архивировано 14 июля 2014 года.
↑ Архивированная копия (неопр.). Дата обращения: 9 декабря 2016. Архивировано из оригинала 14 июля 2014 года.Архивированная копия (неопр.). Дата обращения: 9 декабря 2016. Архивировано 14 июля 2014 года.
↑ Gérard Huet. Архивная копия от 12 сентября 2008 на Wayback Machine
↑ Sanskrit Heritage Site (неопр.). Дата обращения: 9 декабря 2016. Архивировано 3 июня 2013 года.
↑ The Herbrand Award for Distinguished Contributions to Automated Reasoning (неопр.). Дата обращения: 9 декабря 2016. Архивировано из оригинала 7 февраля 2015 года.
↑ The European Association for Theoretical Computer Science Award (неопр.). Дата обращения: 9 декабря 2016. Архивировано 21 декабря 2016 года.