Le développement du prouveur de théorèmes interactif Rocq constitue la contribution technique principale de Christine Paulin-Mohring. Informaticienne et logicienne mathématicienne française née en 1962, ses recherches se concentrent sur la formalisation du raisonnement mathématique à travers des systèmes informatiques. Son parcours académique couvre des décennies de leadership institutionnel et de contributions à la vérification rigoureuse de logiciels et de preuves au sein de la communauté scientifique mondiale.
Fondations académiques et carrière
Paulin-Mohring a terminé ses études doctorales en 1989 sous la direction de Gérard Huet. Sa carrière est ancrée dans l'enseignement supérieur français, plus précisément à l'Université Paris Diderot où elle a achevé sa formation. Depuis 1997, elle occupe une chaire de professeure à l'Université Paris-Saclay. Ses fonctions administratives incluent le poste de doyenne de la Faculté des sciences de l'Université Paris-Saclay de 2016 à 2021, et elle a agi en tant que coordinatrice scientifique du Labex DigiCosme entre 2012 et 2015.
Contributions à la preuve de théorèmes
Le système Rocq, anciennement identifié comme Coq, représente une avancée significative dans la preuve interactive de théorèmes. Paulin-Mohring a collaboré avec une équipe de développement comprenant Thierry Coquand, Gérard Huet, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot et Pierre Castéran. Cet effort collectif a fourni des outils pour formaliser la logique et vérifier des preuves mathématiques, menant à sa participation active au comité éditorial du Journal of Formalized Reasoning.
Reconnaissance professionnelle
L'Association for Computing Machinery a reconnu l'équipe de développement de Rocq avec le prix ACM Software System en 2013. Deux ans plus tard, l'Académie des sciences française a décerné à Paulin-Mohring le prix Michel Monpetit. Elle a été élue membre de l'Academia Europaea en 2014, reflétant son statut au sein de la communauté scientifique européenne.
Vingt questions, huit minutes au chronomètre et un centile mesuré face à tous ceux qui l’ont passé. Sans inscription.
Passer le test de QI →Faits en bref
- Naissance : 1962 - Nationalité : France - Éducation : Université Paris Diderot - Employeur actuel : ComUE Université Paris-Saclay - Projet majeur : Prouveur de théorèmes Rocq - Prix ACM Software System : 2013 - Prix Michel Monpetit : 2015 - Membre de l'Academia Europaea depuis : 2014
Questions posées par les lecteurs
### Quel est le principal domaine académique de Christine Paulin-Mohring ?
Elle est logicienne mathématicienne et informaticienne spécialisée dans la preuve interactive de théorèmes.
### À quel système logiciel majeur est-elle associée ?
Elle est connue pour ses travaux sur le prouveur de théorèmes interactif appelé Rocq, anciennement nommé Coq.
.jpg)