Юэ, Жерар
| Жерар Юэ | |
|---|---|
| фр. Gérard Huet | |
 | |
| Дата рождения | 7 июля 1947 (77 лет) |
| Место рождения | Бурж |
| Страна | |
| Род деятельности | специалист в области информатики, инженер, логик, преподаватель университета, математик |
| Научная сфера | Математика |
| Место работы | Парижский университет |
| Альма-матер | Университет Кейс Вестерн Резерв Университет Париж Дидро |
| Научный руководитель | Морис Нива |
| Ученики | Benoît Razet[вд][1] |
| Награды и премии | |
| Сайт | 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 года.
Ссылки
[править | править код]- Юэ, Жерар (англ.) в проекте «Математическая генеалогия»
- Gérard Huet’s home page Архивная копия от 28 ноября 2016 на Wayback Machine
- Gérard Huet Héritage du sanskrit dictionnaire sanskrit-français. Дата обращения: 9 декабря 2016. Архивировано 27 февраля 2008 года. (3.32 MB) (428 pages, 5 April 2007)
