Дэмиен Долигез
Дэмиен Долигез | |
|---|---|
 Дэмиен Долигез | |
| Национальность | Французский |
| Альма-матер | Ecole Normale Superieure (Париж) |
| Известный | OCaml |
| Научная карьера | |
| Поля | Информатика |
| Учреждения | Инрия |
| Диссертация | Проектирование, изготовление и сертификация конкурирующей машины для сбора клеток (1995 г.) |
| Докторантура | Жан-Жак Леви [1] |
Дэмиен Долигез — французский академик и программист . Он наиболее известен своей ролью разработчика системы OCaml , особенно ее сборщика мусора . Он является научным сотрудником ( поверенный в исследованиях ) во французском государственном научно-исследовательском институте INRIA .
Деятельность
[ редактировать ]В 1990 году Долигез и Ксавье Лерой построили реализацию Caml (названную Caml Light) на основе байт-кода интерпретатора с быстрым последовательным сборщиком мусора и начали расширять ее за счет поддержки параллелизма. [2] В 1996 году Долигез был частью команды, создавшей первую версию OCaml . [3] и с тех пор (по состоянию на апрель 2023 года) является основным сопровождающим языка. [4]
В 1994 году Хэл Финни бросил вызов [5] в рассылке шифропанка , чтобы прочитать зашифрованный сеанс SSLv2 . Долигез использовал запасные компьютеры в Inria , ENS и Политехнической школе, чтобы сломать его после сканирования половины ключевого пространства за 8 дней. [6] Он занял второе место в соревновании, а команда-победитель объявила свой результат всего двумя часами ранее. [7] [8]
С 2006 года Долигез участвует в разработке Zenon. [9] средство доказательства теорем для классической логики первого порядка с равенством. Зенон — двигатель [10] который управляет Focalize [11] среда программирования, которая может проектировать и разрабатывать сертифицированные программы.Среда основана на функциональном языке с некоторыми объектно-ориентированными функциями, что позволяет программистам писать формальную спецификацию идоказательства их кода в одной и той же обстановке. Создание доказательств осуществляется с помощью Zenon, а результаты формально проверяются машиной с помощью средства проверки доказательств Coq .
В 2008 году Долигез работал с Лесли Лэмпортом и другими над созданием менеджера доказательств TLA+ , который поддерживает поэтапную разработку и проверку иерархически структурированных компьютерных доказательств . [12] Проект менеджера доказательств продолжает активно поддерживаться и развиваться по состоянию на 2022 год. [13]
Ссылки
[ редактировать ]- ^ Леви, Жан-Жак. «Домашняя страница Жан-Жака Леви» .
- ^ Долигез, Дэмиен; Лерой, Ксавье (январь 1993 г.). Параллельный сборщик мусора с генерацией для многопоточной реализации ML . 20-й симпозиум ACM по принципам языков программирования (POPL). АКМ .
- ^ Анил Мадхавапедди и Ярон Мински (декабрь 2022 г.). «Реальный мир OCaml: Пролог» .
- ^ «О OCaml» . 2023.
- ^ Хэл Финни (1994). «SSL-вызов» . Архивировано из оригинала 10 августа 2001 г.
- ^ Дэмиен Долигез (1995). «Объявить о решении проблемы SSL» .
- ^ Ричард Клейтон. «Атака методом грубой силы на криптографические ключи» .
- ^ Дэмиен Долигез. «Виртуальная конференция SSL Challenge» .
- ^ Боничон, Ричард; Делахай, Дэвид; Долигез, Дэмиен (2007). Zenon: расширяемое автоматическое средство доказательства теорем, производящее проверяемые доказательства . LPAR 2007 — 14-я Международная конференция по логике программирования, искусственному интеллекту и рассуждению. Спрингер. дои : 10.1007/978-3-540-75560-9_13 .
- ^ Гитхаб (2023 г.). «Доказывающая Зенона» . Гитхаб .
- ^ Дэмиен Долигез (2022). «Основное фокусирование» . Инрия.
- ^ Чаудхури, Каустав (12 ноября 2008 г.). «Система доказательства TLA+». arXiv : 0811.1914 [ cs.LO ].
- ^ Гитхаб (2023 г.). «Менеджер проверки TLA» . Гитхаб .
Внешние ссылки
[ редактировать ]ML- программирование | |||
|---|---|---|---|
| Программное обеспечение |
|  | |
| Сообщество |
| ||
| Базы данных авторитетного контроля : академики |
|---|
