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

Биография

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

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

Является автором для просто типизированного лямбда-исчисления и полного доказательства метод теории типов Чёрча . Он работал над редактором программы Mentor в 1974—1977 годах с Жилем Каном . В 1978—1984 годах работал над КБ эквациональной системой доказательств совместно с Жаном-Мари Юлло . Возглавлял проект Formel в 1980-х годах, который разработал язык программирования Caml. В 1984 году разработал исчисление конструкций совместно с Тьерри Коканом . Возглавлял проект Coq в 1990-х годах с Кристин Полин, разрабатывавшей проверку ассистента Coq . Изобрел структуру данных в 1996. Был руководителем международных отношений INRIA в 1996—2000 гг. Разработал в 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 prévision-réalisation des vols , Société d’informatique, de conseils et de recherche opérationnelle (SINCRO), Paris, 1970. от 20 декабря 2016 на Wayback Machine
• Spécifications pour une base commune de données , SINCRO, Paris, 1971. от 4 апреля 2016 на Wayback Machine
• Gérard P. Huet. A Mechanization of Type Theory // (англ.) / Nils J. Nilsson. — William Kaufmann, 1973. — P. 139—146.
• Gérard P. Huet. (англ.) // (англ.) ( : journal. — 1973. — Vol. 22 . — P. 257—267 . — doi : .
• La Gestion des données dans les systèmes informatiques , École supérieure d'électricité, Malakoff, 1974. от 4 апреля 2016 на Wayback Machine
• , 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 (англ.) // (англ.) ( : journal. — 1978. — Vol. 11 . — P. 31—55 . — doi : .
• Gérard Huet, D.S. Lankford. (англ.) . — 1978. — P. 8.

• G. Huet, J.M. Hullot. Proofs by Induction in Equational Theories with Constructors // (англ.) . — Institute of Electrical and Electronics Engineers , 1980. — P. 96—107.
• G. Huet, D.C. Oppen. (неопр.) . — 1980. — С. 52.
• Gérard Huet. (англ.) // J. Comput. System Sci. : journal. — 1981. — Vol. 23 . — P. 11—21 . — doi : .
• Gérard Huet. (англ.) . — 1986. — (International Summer School on Logic of Programming and Calculi of Discrete Design). от 14 июля 2014 на Wayback Machine
• Gérard Huet. (англ.) / K. Fuchi and M. Nivat. — North-Holland, 1988. — P. 205—216. от 1 июля 2015 на Wayback Machine

• Gérard Huet. (англ.) . — 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 // (неопр.) / M. Abadi and T. Ito. — Springer, 1997. — Т. 1281. — С. 604—610. — (LNCS). от 22 декабря 2014 на Wayback Machine
• Gérard Huet. (неопр.) // Math. Struct. in Comp. Science. — 1998. — Т. 8 . — С. 671—680 . — doi : . 24 января 2016 года.

• Gérard Huet. Higher Order Unification 30 years later // (англ.) / V. Carreño and C. Muñoz and S. Tahar. — Springer, 2002. — Vol. 2410. — P. 3—12. — (LNCS).
• Gérard Huet. (англ.) / Fairouz Kamareddine. — (англ.) ( , 2003. от 1 июля 2015 на Wayback Machine

Примечания

Ссылки

• (англ.) в проекте « Математическая генеалогия »
• от 28 ноября 2016 на Wayback Machine
• (неопр.) . Дата обращения: 9 декабря 2016. 27 февраля 2008 года. (3.32 MB) (428 pages, 5 April 2007)