Крістін Полін-Мохрінг (фр. Christine Paulin-Mohring нар. 31 травня 1962Birth year from Library of Congress catalog entry) - французька математикиня-інформатикиня, дослідниця та викладачка на факультеті наук університету Париж-Сакле. Найбільш відома за розробку помічника доведення теорем Rocq.
Біографія Крістін Полін-Мохрінг здобула свою докторантуру у 1989 році під керівництвом Жерард Хуета. Її дисертація була присвячена вилученню програм з обчислень конструкційThèse de Christine Paulin..
Після того як вона була призначена керувати дослідженням в Національному центрі наукових досліджень (НЦНД) в лабораторії інформатики паралелізму у Вищій Педагогічній Школі міста Льйон (ENS Lyon), вона працює професоркою в університеті Париж-Сакле(в минулому Університет Париж XI) з 1997 року.. Її дисертація на здобуття наукового ступеня з керівництвом науковими дослідженнями була присвячена індуктивним визначенням у теорії типівДисертація Крістіни Полін..
Між 2012 і 2015 роками вона була науковим координатором "Labex DigiCosme".. Вона є членом комітету з редакції журналу ..
Вона працювала разом з Жерард Хуетом і Ть'єрі Кокяном над інтерактивним демонстратором теорем у Inria(Національний науково-дослідний інститут). Мова йде про програмне забезпечення Rocq, Помічник доведення теорем. Жерард Хует і Ть'єрі Кокян розробляють логіку програмного забезпечення та розрахунки конструкцій. Крістін Полін-Мохрінг імплементує нову консрукцію: індуктивні типи та механізм вилучення, що дозволяє автоматично отримати програму без помилок на основі доказу. Це позволяє верифікувати складні математичні обчислення. На приклад, Жорж Ґонтьє і його команда довели теорему чотирьох кольорів, яка стверджує що кожна карта може бути розфарбована лише чотирма кольорами, забезпечуючи що дві суміжні області завжди отримують два окремі кольори. Внесок Крістін Полін-Мохрінг полягає в тому що доказ перевірений програмним забезпеченням Rocq може бути перетворений у програму "нульових дефектів", тобто без помилок, відповідно до специфікацій. Вплив програмного забезпечення Rocq дуже важливий для навукового співтовариства..
Нагороди та відзнаки prix Michel-Monpetit , Французька академія наук, 2015.. нагорода ACM SIGPLAN Programming Languages Software, за проєкт Rocq, Association for Computing Machinery, 2013. нагорода ACM Software System, за проєкт Rocq, Association for Computing Machinery, 2013..
Видання
Lecture Notes in Computer Science. Types for Proofs and Programs: International Workshop TYPES'96, Aussois, France, 15–19 December 1996 Selected Papers; Eduardo Gimenez, Christine Paulin-Mohring, Springer Types for Proofs and Programs: International Workshop, TYPES 2004, Jouy-en-Josas, France, 15–18 December 2004, Revised Selected Papers: 3839 (Lecture Notes in Computer Science); Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner, Springer, 2008 Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, 22–26 July 2013, Proceedings (Lecture Notes in Computer Science); Sandrine Blazy, Christine Paulin-Mohring, David Pichardie, Springer, 2013
Джерела