交互式定理证明器Rocq的开发是克里斯蒂娜·波兰-莫林 (Christine Paulin-Mohring) 的主要技术贡献。作为一位1962年出生的法国计算机科学家和数理逻辑学家，她的研究专注于通过计算系统实现数学推理的规范化。她的学术生涯涵盖了数十年的机构领导工作，以及为全球科学界在软件和证明的严谨验证方面做出的贡献。
学术背景与职业生涯
波兰-莫林于1989年在杰拉德·于埃 (Gérard Huet) 的指导下完成了博士学业。她的职业生涯根植于法国高等教育系统，特别是她曾就读的巴黎狄德罗大学。自1997年以来，她一直在巴黎-萨克雷大学担任教授职务。她的行政职务包括从2016年至2021年担任巴黎-萨克雷大学理学院院长，并于2012年至2015年间担任Labex DigiCosme的科学协调员。
对定理证明的贡献
Rocq系统（原名Coq）代表了交互式定理证明领域的一项重大进展。波兰-莫林曾与一个开发团队合作，成员包括蒂埃里·科康 (Thierry Coquand)、杰拉德·于埃、布鲁诺·巴拉斯 (Bruno Barras)、让-克里斯托弗·菲利亚特尔 (Jean-Christophe Filliâtre)、雨果·埃尔伯林 (Hugo Herbelin)、切坦·默西 (Chetan Murthy)、伊夫·贝尔托 (Yves Bertot) 和皮埃尔·卡斯特朗 (Pierre Castéran)。这一集体努力提供了用于逻辑规范化和数学证明验证的工具，使她得以活跃于《形式化推理杂志》(Journal of Formalized Reasoning) 的编辑委员会中。
专业认可
计算机协会 (ACM) 于2013年授予Rocq开发团队ACM软件系统奖。两年后，法国科学院授予波兰-莫林米歇尔·蒙佩蒂奖 (Prix Michel Monpetit)。2014年，她当选为欧洲科学院 (Academia Europaea) 成员，这体现了她在欧洲科学研究界的重要地位。
快速事实
- 出生年份: 1962年 - 国籍: 法国 - 教育背景: 巴黎狄德罗大学 - 当前任职单位: 巴黎-萨克雷大学 (ComUE) - 主要项目: Rocq定理证明器 - ACM软件系统奖: 2013年 - 米歇尔·蒙佩蒂奖: 2015年 - 欧洲科学院成员入选年份: 2014年
读者常见问题
### 克里斯蒂娜·波兰-莫林的主要学术研究重点是什么？
她是一位专门研究交互式定理证明的数理逻辑学家和计算机科学家。
### 她与哪项重大软件系统相关联？
她因在被称为Rocq（原名Coq）的交互式定理证明器方面的工作而闻名。
.jpg)