Юэ, Жерар

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

Биография

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

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

Является автором алгоритма унификации для просто типизированного лямбда-исчисления и полного доказательства метод теории типов Чёрча. Он работал над редактором программы Mentor в 1974—1977 годах с Жилем Каном. В 1978—1984 годах работал над КБ эквациональной системой доказательств совместно с Жаном-Мари Юлло. Возглавлял проект Formel в 1980-х годах, который разработал язык программирования Caml. В 1984 году разработал Calculus of constructions совместно с Тьерри Коканом. Возглавлял проект Coq в 1990-х годах с Кристин Полин, разрабатывавшей проверку ассистента Coq. Изобрел структуру данных 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. Совсем недавно он был ученым по компьютерной лингвистике на санскрите. Является веб-мастером сайта the Sanskrit Heritage Site.

Юэ получил премию Эрбрановы в 1998 году и премию EATCS в 2009 году.

Публикации

• Le Projet prvision-ralisation des vols, Socit d’informatique, de conseils et de recherche oprationnelle (SINCRO), Paris, 1970. WorldCat Record
• Spcifications pour une base commune de donnes, SINCRO, Paris, 1971. WorldCat Record
• Grard 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.
• Grard P. Huet (1973). «The Undecidability of Unification in Third Order Logic». Information and Control 22: 257–267. DOI:10.1016/s0019-9958(73)90301-x.
• La Gestion des donnes dans les systmes informatiques, cole suprieure d'lectricit, Malakoff, 1974. WorldCat Record
• «A Unification Algorithm for Typed Lambda-Calculus», Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
• Grard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,... (Ph.D.). Universite de Paris VII. 
• Grard Huet, Bernard Lang (1978). «Proving and Applying Program Transformations Expressed with Second-Order Patterns». Acta Informatica 11: 31–55. DOI:10.1007/bf00264598.
• Grard Huet, D.S. Lankford. On the Uniform Halting Problem for Term Rewriting Systems. — P. 8.

• G. Huet, J.M. Hullot. Proofs by Induction in Equational Theories with Constructors // 21st Ann. Symp. on Foundations of Computer Science. — IEEE. — P. 96–107.
• G. Huet, D.C. Oppen. Equations and Rewrite Rules: A Survey. — P. 52.
• Grard Huet (1981). «A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm». J. Comput. System Sci. 23: 11–21. DOI:10.1016/0022-0000(81)90002-7.
• Grard Huet. Formal Structures for Computation and Deduction.
• Grard Huet. Induction Principles Formalized in the Calculus of Constructions / K. Fuchi and M. Nivat. — North-Holland, 1988. — P. 205–216.

• Grard Huet. Residual Theory in -Calculus: A Formal Development.
• Huet, G.P. Design Proof Assistant (invited lecture) / Ganzinger, Harald. — Springer-Verlag, 1996. — Vol. 1103. — P. 153.
• Grard Huet, H. Laulhre. Finite-state Transducers as Regular Bhm Trees // Theoretical Aspects of Computer Software / M. Abadi and T. Ito. — Springer. — Vol. 1281. — P. 604–610.
• Grard Huet (1998). «Regular Bhm Trees». Math. Struct. in Comp. Science 8: 671–680. DOI:10.1017/s0960129598002643.

• Grard Huet. Higher Order Unification 30 years later // Proceedings, 15th International Conference TPHOL / V. Carreo and C. Muoz and S. Tahar. — Springer, 2002. — Vol. 2410. — P. 3–12. Postscript
• Grard Huet. Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation / Fairouz Kamareddine. — Kluwer, 2003.