Christine Paulin-Mohring
# Christine Paulin-Mohring

Christine Paulin-Mohring (* 31. Mai 1962) ist eine französische Mathematikerin und Informatikerin. Sie entwickelte mit anderen die Coq-Software, eine Software zum maschinengestützten Beweisen.

## Leben

Christine Paulin-Mohring promovierte 1989 an der Universität Paris VII unter der Leitung von Gérard Huet. Seit 1997 ist sie Professorin an der Universität Paris-Süd.
Zwischen 2012 und 2015 war sie wissenschaftliche Koordinatorin des Labex DigiCosme. Derzeit ist sie Mitglied des Redaktionsausschusses des Journal of Formalized Reasoning.
Beim Informatikinstitut Institut national de recherche en informatique et en automatique (Inria) arbeitet sie zusammen mit Gérard Huet und Thierry 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 das Vier-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ß.
Seit 2016 ist sie Dekanin der Fakultät für Naturwissenschaften an der Universität Paris-Süd.

## Preise und Auszeichnungen

* Michel-Monpetit-Preis der Académie des sciences, 2015.
* Mitglied der Academia Europaea seit 2014.
* ACM SIGPLAN Programming Languages Software Award der Association for Computing Machinery für das Coq-Projekt, 2013.
* ACM Software System Award der Association for Computing Machinery für das Coq-Projekt, 2013.
* Ehrendoktor der Universität Göteborg.