Разработка интерактивного верификатора теорем Rocq является основным техническим вкладом Кристин Полен-Морен (Christine Paulin-Mohring). Будучи французским специалистом в области информатики и математической логики, родившейся в 1962 году, она сосредоточила свои исследования на формализации математических рассуждений с помощью вычислительных систем. Ее академический путь охватывает десятилетия институционального руководства и вклада в строгую верификацию программного обеспечения и доказательств в мировом научном сообществе.
Академический фундамент и карьера
Полен-Морен завершила докторантуру в 1989 году под руководством Жерара Юэ (Gérard Huet). Ее карьера неразрывно связана с французской системой высшего образования, в частности с Университетом Париж Дидро, где она получила свое образование. С 1997 года она занимает должность профессора в Университете Париж-Сакле. Ее административная деятельность включает работу в качестве декана факультета наук Париж-Сакле с 2016 по 2021 год, а также роль научного координатора Labex DigiCosme в период с 2012 по 2015 год.
Вклад в доказательство теорем
Система Rocq, ранее известная как Coq, представляет собой значительный шаг вперед в области интерактивного доказательства теорем. Полен-Морен сотрудничала с командой разработчиков, в которую входили Тьерри Кокан (Thierry Coquand), Жерар Юэ, Бруно Баррас (Bruno Barras), Жан-Кристоф Фийятр (Jean-Christophe Filliâtre), Юго Эрбелен (Hugo Herbelin), Четан Мурти (Chetan Murthy), Ив Берто (Yves Bertot) и Пьер Кастеран (Pierre Castéran). Эти совместные усилия позволили создать инструменты для формализации логики и проверки математических доказательств, что привело к ее активному участию в редакционном совете журнала Journal of Formalized Reasoning.
Профессиональное признание
Ассоциация вычислительной техники (ACM) отметила команду разработчиков Rocq премией ACM Software System Award в 2013 году. Два года спустя Французская академия наук вручила Полен-Морен премию Мишеля Монпети (Prix Michel Monpetit). В 2014 году она была избрана членом Европейской академии (Academia Europaea), что отражает ее высокий статус в европейском научном сообществе.
Двадцать вопросов, восемь минут на часах и процентиль, измеренный по всем, кто его проходил. Без регистрации.
Пройти тест IQ →Краткие факты
- Год рождения: 1962 - Гражданство: Франция - Образование: Университет Париж Дидро - Текущий работодатель: ComUE Университет Париж-Сакле - Основной проект: Верификатор теорем Rocq - Премия ACM Software System Award: 2013 - Премия Мишеля Монпети: 2015 - Член Европейской академии с: 2014 года
Вопросы читателей
### Какова основная академическая специализация Кристин Полен-Морен?
Она является математическим логиком и компьютерным ученым, специализирующимся на интерактивном доказательстве теорем.
### С какой крупной программной системой она связана?
Она известна своей работой над интерактивным верификатором теорем, известным как Rocq, ранее называвшимся Coq.
.jpg)