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. Die Coq-Software hat einen erheblichen Einfluss auf die wissenschaftliche Gemeinschaft gehabt.
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.
Einzelnachweise
Kategorie:Mitglied der Academia Europaea Kategorie:Ehrendoktor der Universität Göteborg Kategorie:Mathematiker (21. Jahrhundert) Kategorie:Informatiker Kategorie:Hochschullehrer (Paris) Kategorie:Franzose Kategorie:Geboren 1962 Kategorie:Frau