Christine Paulin-Mohring (*31. Mai1962)[1] ist eine französischeMathematikerin undInformatikerin. Sie entwickelte mit anderen dieCoq-Software, eine Software zummaschinengestützten Beweisen.
Christine Paulin-Mohring promovierte 1989 an derUniversität Paris VII unter der Leitung vonGérard Huet. Seit 1997 ist sieProfessorin an derUniversität Paris-Süd.[2]
Zwischen 2012 und 2015 war sie wissenschaftliche Koordinatorin des Labex DigiCosme.[3] Derzeit ist sie Mitglied des Redaktionsausschusses desJournal of Formalized Reasoning.[4]
Beim InformatikinstitutInstitut national de recherche en informatique et en automatique (Inria) arbeitet sie zusammen mit Gérard Huet undThierry Coquand an der Coq-Software, einer interaktiven Theorembeweis-Maschine. Thierry Coquand und Gérard Huet entwickeln die Logik der Software und die Berechnung der Konstruktionen. Christine Paulin-Mohring implementiert eine neue Konstruktion: induktive Typen und einen Extraktionsmechanismus, der automatisch ein Null-Fehler-Programm aus einem Beweis erhält. Auf diese Weise lassen sich wichtige mathematische Berechnungen nachprüfen. Georges Gonthier und sein Team bestätigten beispielsweise dasVier-Farben-Satz, der besagt, dass jede Karte mit nur vier Farben eingefärbt werden kann, wobei sichergestellt wird, dass zwei benachbarte Regionen immer zwei unterschiedliche Farben erhalten. Der Beitrag von Christine Paulin-Mohring besteht darin, dass ein von der Coq-Software verifizierter Beweis in ein fehlerfreies, d. h. spezifikationskonformes Programm umgewandelt werden kann. Der Einfluss der Coq-Software auf die wissenschaftliche Gemeinschaft ist sehr groß.[5]
Seit 2016 ist sieDekanin der Fakultät für Naturwissenschaften an der Universität Paris-Süd.[6]
| Personendaten | |
|---|---|
| NAME | Paulin-Mohring, Christine |
| KURZBESCHREIBUNG | französische Mathematikerin und Informatikerin |
| GEBURTSDATUM | 31. Mai 1962 |