Interested Article - Леруа, Ксавье

Ксавье Леруа ( фр. Xavier Leroy ; род. 15 марта 1968 года ) — французский информатик и программист. Известен как основной разработчик системы OCaml .

Старший научный сотрудник ( фр. directeur de recherche) французского государственного научно-исследовательского учреждения INRIA . Леруа был принят в Эколь Нормаль в Париже в 1987 году, где он изучал математику и информатику. С 1989 по 1992 он защитил кандидатскую диссертацию в области компьютерных наук под руководством Жерара Юэ .

Является международно признанным экспертом по языкам и компиляторам функционального программирования . В последнее время приобрёл интерес к формальным методам , формальным проверкам и сертифицированной компиляции. Он является руководителем проекта CompCert , который разрабатывает оптимизирующий компилятор для С , формально верифицированный в Coq .

Леруа был также оригинальным автором LinuxThreads , наиболее широко используемого пакета, реализующего потоки пакета в ОС Linux с версиями ядра Linux 2.0 , 2.2, 2.4. Вместе с ядром Linux 2.6 в качестве замены LinuxThreads была введена библиотека NPTL , с гораздо более широкой поддержкой со стороны ядра.

В 2015 был объявлен действительным членом Ассоциации вычислительной техники «за вклад в безопасные, высокоэффективные функциональные языки программирования и компиляторы, и верификацию компилятора». В 2016 был удостоен британским Лондонским королевским обществом и премии ван Вейнгаардена нидерландским Центром математики и информатики .

Примечания

↑ (фр.) — Paris: 1953. — ISSN ;
от 13 августа 2010 на Wayback Machine «It runs on any Linux system with kernel 2.0.0»
, Association for Computing Machinery , 2015 , < > . Проверено 9 декабря 2015. (неопр.) . Дата обращения: 12 декабря 2016. Архивировано из 9 декабря 2015 года. .
(неопр.) . Royal Society. Дата обращения: 19 ноября 2015. 6 сентября 2018 года.
от 25 сентября 2016 на Wayback Machine .