פיתוח מערכת ההוכחה האינטראקטיבית Rocq עומד כתרומה הטכנית העיקרית של קריסטין פולין-מורינג (Christine Paulin-Mohring). היא מדענית מחשב ולוגיקנית מתמטית צרפתייה שנולדה ב-1962, ומחקרה מתמקד בפורמליזציה של הסקה מתמטית באמצעות מערכות חישוביות. המסלול האקדמי שלה משתרע על פני עשורים של הובלה מוסדית ותרומות לאימות קפדני של תוכנה והוכחות בתוך הקהילה המדעית העולמית.
תשתית אקדמית וקריירה
פולין-מורינג השלימה את לימודי הדוקטורט שלה ב-1989 בהנחייתו של ז'ראר אווה (Gérard Huet). הקריירה שלה נטועה בהשכלה הגבוהה בצרפת, ובאופן ספציפי באוניברסיטת פריז דידרו (Paris Diderot University) שבה השלימה את הכשרתה. מאז 1997, היא מחזיקה במשרת פרופסור באוניברסיטת פריז-סאקלה (Paris-Saclay University). תפקידיה האדמיניסטרטיביים כוללים כהונה כדיקנית הפקולטה למדעים של פריז-סאקלה משנת 2016 ועד 2021, והיא שימשה כמתאמת המדעית של Labex DigiCosme בין השנים 2012 ו-2015.
תרומות להוכחת משפטים
מערכת Rocq, שזוהתה בעבר כ-Coq, מייצגת התקדמות משמעותית בהוכחת משפטים אינטראקטיבית. פולין-מורינג שיתפה פעולה עם צוות פיתוח שכלל את תיירי קוקאן (Thierry Coquand), ז'ראר אווה, ברונו באראס (Bruno Barras), ז'אן-כריסטוף פיליאטר (Jean-Christophe Filliâtre), הוגו הרבלין (Hugo Herbelin), צ'טן מרתי (Chetan Murthy), איב ברטו (Yves Bertot) ופייר קסטראן (Pierre Castéran). מאמץ קולקטיבי זה סיפק כלים לפורמליזציה של לוגיקה ואימות הוכחות מתמטיות, מה שהוביל להשתתפותה הפעילה במועצת העריכה של כתב העת Journal of Formalized Reasoning.
הכרה מקצועית
האגודה למכונות מחשוב (ACM) הכירה בצוות הפיתוח של Rocq עם פרס ACM למערכות תוכנה (ACM Software System Award) בשנת 2013. שנתיים לאחר מכן, האקדמיה הצרפתית למדעים העניקה לפולין-מורינג את פרס מישל מונפטי (Michel Monpetit Prize). היא נבחרה כחברה באקדמיה אירופיאה (Academia Europaea) בשנת 2014, דבר המשקף את מעמדה בתוך הקהילה המדעית האירופית.
Twenty questions, eight minutes on the clock, and a percentile measured against everyone who has taken it. No sign-up.
Take the IQ test →עובדות מהירות
- נולדה: 1962 - אזרחות: צרפת - השכלה: אוניברסיטת פריז דידרו - מעסיק נוכחי: אוניברסיטת פריז-סאקלה - פרויקט עיקרי: מוכיח המשפטים Rocq - פרס ACM למערכות תוכנה: 2013 - פרס מישל מונפטי: 2015 - חברה באקדמיה אירופיאה מאז: 2014
שאלות שקוראים שואלים
### מהו המיקוד האקדמי העיקרי של קריסטין פולין-מורינג?
היא לוגיקנית מתמטית ומדענית מחשב המתמחה בהוכחת משפטים אינטראקטיבית.
### עם איזו מערכת תוכנה מרכזית היא מזוהה?
היא ידועה בעבודתה על מוכיח המשפטים האינטראקטיבי הידוע בשם Rocq, שנקרא בעבר Coq.