Лерой, Ксавье
Ксавье Леруа (фр. Xavier Leroy; род. 15 марта 1968[1], Орлеан[2]) — французский информатик и программист. Профессор Коллеж де Франс (с 2018 года)[3], член Французской академии наук (с 2022 года)[4]. Известен как разработчик языка OCaml и верифицированного компилятора CompCert.
Общие сведения
| Ксавье Лерой | |
|---|---|
| Дата рождения | 15 марта 1968[1] (58 лет) |
| Место рождения | |
| Страна | |
| Научная сфера | информатика и функциональное программирование |
| Место работы | |
| Образование | |
| Научный руководитель | Юэ, Жерар |
| Награды и премии |
премия Мишеля Монпети[d] (2007) премия Милнера[d] (2016) премия ван Вейнгаардена[d] (2016) член Ассоциации вычислительной техники (2015) Большая премия INRIA и Французской академии наук[d] (2018) |
Биография
В 1987 году Леруа поступил в Высшую нормальную школу в Париже, где изучал математику и информатику. В 1992 году он защитил докторскую диссертацию по информатике под руководством Жерара Юэ. В 1993—1994 годах проходил постдокторантуру в Стэнфордском университете[5].
В 1994 году начал работать в INRIA, где в 2000 году занял пост директора по исследованиям. С 2006 по 2019 год руководил исследовательской группой Gallium[3]. В 1999—2004 годах также работал научным консультантом в компании Trusted Logic[6].
В мае 2018 года был назначен профессором Коллеж де Франс, где возглавил кафедру «Науки о программном обеспечении»[3].
В 2022 году избран членом Французской академии наук[4].
Научная деятельность
Ксавье Леруа является основным разработчиком языка программирования OCaml. Эволюция языка началась с реализации Caml Light (1990) и Caml Special Light (1995), в которую были добавлены нативный компилятор и система модулей. В 1996 году была выпущена версия OCaml[7].
С 2005 года учёный руководит проектом CompCert — разработкой формально верифицированного компилятора языка Си. Проект использует ассистент доказательств Coq для гарантии того, что сгенерированный код семантически эквивалентен исходной программе[8].
Леруа также является автором библиотеки LinuxThreads[9], обеспечивавшей поддержку потоков в Linux. Она широко использовалась в ядрах версий 2.0—2.4, пока в версии 2.6 не была заменена на NPTL.
Награды и признание
- 2015 — Действительный член Ассоциации вычислительной техники (ACM Fellow) «за вклад в безопасные, высокоэффективные функциональные языки программирования и компиляторы, и верификацию компилятора».
- 2016 — Премия Милнера от Лондонского королевского общества[10].
- 2016 — Премия ван Вейнгаардена от Центра математики и информатики (Нидерланды).
- 2021 — ACM Software System Award за разработку CompCert[6].
- 2022 — избран членом Французской академии наук[4].
- 2022 — ACM SIGPLAN Programming Languages Software Award за систему OCaml[11].
