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.
Leben
[Bearbeiten | Quelltext bearbeiten]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]
Preise und Auszeichnungen
[Bearbeiten | Quelltext bearbeiten]- 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]
Einzelnachweise
[Bearbeiten | Quelltext bearbeiten]- ↑ Notice de personne. In: catalogue.bnf.fr. BnF, abgerufen am 28. November 2021 (französisch).
- ↑ Short biography. In: lri.fr. Laboratoire de recherche en informatique, abgerufen am 28. November 2021 (englisch).
- ↑ Christine Paulin-Mohring. In: lri.fr. Laboratoire de recherche en informatique, abgerufen am 28. November 2021 (englisch).
- ↑ Journal of Formalized Reasoning, Editorial Team. In: jfr.unibo.it. Journal of Formalized Reasoning, abgerufen am 28. November 2021 (englisch).
- ↑ Christine Paulin et les Logiciels Zéro Défaut. In: lemonde.fr. Le Monde, 24. September 2015, abgerufen am 28. November 2021 (französisch).
- ↑ 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 (nicht mehr online verfügbar) am 28. November 2021; abgerufen am 28. November 2021 (französisch).
- ↑ Lauréats 2015 des prix thématiques. In: academie-sciences.fr. Académie des Sciences, 2015, abgerufen am 28. November 2021 (französisch).
- ↑ Christine Paulin-Mohring. In: ae-info.org. Academia Europaea, abgerufen am 28. November 2021 (englisch).
- ↑ Christine Paulin-Mohring, ACM Software System AQward. In: awards.acm.org. Association for Computing Machinery, 2013, archiviert vom (nicht mehr online verfügbar) am 28. November 2021; abgerufen am 28. November 2021 (englisch).
| Personendaten | |
|---|---|
| NAME | Paulin-Mohring, Christine |
| KURZBESCHREIBUNG | französische Mathematikerin und Informatikerin |
| GEBURTSDATUM | 31. Mai 1962 |