Christine Paulin-Mohring

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

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.^[2]

Zwischen 2012 und 2015 war sie wissenschaftliche Koordinatorin des Labex DigiCosme.^[3] Derzeit ist sie Mitglied des Redaktionsausschusses des Journal of Formalized Reasoning.^[4]

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ß.^[5]

Seit 2016 ist sie Dekanin der Fakultät für Naturwissenschaften an der Universität Paris-Süd.^[6]

• Michel-Monpetit-Preis der Académie des sciences, 2015.^[7]
• Mitglied der Academia Europaea seit 2014.^[8]
• 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.^[9]
• Ehrendoktor der Universität Göteborg.^[6]

1. ↑ Notice de personne. In: catalogue.bnf.fr. BnF, abgerufen am 28. November 2021 (französisch). 
2. ↑ Short biography. In: lri.fr. Laboratoire de recherche en informatique, abgerufen am 28. November 2021 (englisch). 
3. ↑ Christine Paulin-Mohring. In: lri.fr. Laboratoire de recherche en informatique, abgerufen am 28. November 2021 (englisch). 
4. ↑ Journal of Formalized Reasoning, Editorial Team. In: jfr.unibo.it. Journal of Formalized Reasoning, abgerufen am 28. November 2021 (englisch). 
5. ↑ Christine Paulin et les Logiciels Zéro Défaut. In: lemonde.fr. Le Monde, 24. September 2015, abgerufen am 28. November 2021 (französisch). 
6. ↑ ^{a b} Christine PAULIN Personnalité qualifiée désignée par le président de l’ENS Paris-Saclay. In: ens-paris-saclay.fr. ENS Paris Saclay, archiviert vom Original (nicht mehr online verfügbar) am 28. November 2021; abgerufen am 28. November 2021 (französisch). 
7. ↑ Lauréats 2015 des prix thématiques. In: academie-sciences.fr. Académie des Sciences, 2015, abgerufen am 28. November 2021 (französisch). 
8. ↑ Christine Paulin-Mohring. In: ae-info.org. Academia Europaea, abgerufen am 28. November 2021 (englisch). 
9. ↑ Christine Paulin-Mohring, ACM Software System AQward. In: awards.acm.org. Association for Computing Machinery, 2013, archiviert vom Original (nicht mehr online verfügbar) am 28. November 2021; abgerufen am 28. November 2021 (englisch).