対話型定理証明器「Rocq」の開発は、クリスティーヌ・ポーラン＝モーラン (Christine Paulin-Mohring) の主要な技術的貢献である。1962年生まれのフランスの計算機科学者であり数理論理学者である彼女の研究は、計算システムを通じた数学的推論の形式化に焦点を当てている。彼女の学術的キャリアは、数十年にわたる組織的なリーダーシップと、世界中の科学コミュニティにおけるソフトウェアおよび証明の厳密な検証への貢献に及んでいる。
学術的基盤とキャリア
ポーラン＝モーランは1989年にジェラール・ユエ (Gérard Huet) の指導のもとで博士課程を修了した。彼女のキャリアはフランスの高等教育に根ざしており、特に自身が訓練を受けたパリ・ディドロ大学（パリ第7大学）が拠点となっている。1997年からはパリ・サクレ大学で教授職を務めている。行政的な役割として、2016年から2021年までパリ・サクレ大学理学部の学部長を務め、2012年から2015年まではLabex DigiCosmeの科学コーディネーターとしても活動した。
定理証明への貢献
かつて「Coq」として知られていたRocqシステムは、対話型定理証明における重要な進歩を表している。ポーラン＝モーランは、ティエリー・コカン (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ソフトウェアシステム賞を授与した。その2年後、フランス科学アカデミーはポーラン＝モーランにミシェル・モンペティ賞 (Prix Michel Monpetit) を授与した。2014年には欧州アカデミー (Academia Europaea) の会員に選出され、欧州の科学研究コミュニティにおける彼女の地位を反映している。
クイックファクト
- 生年: 1962年 - 国籍: フランス - 教育: パリ・ディドロ大学 - 現在の雇用先: パリ・サクレ大学 (ComUE) - 主要プロジェクト: Rocq定理証明器 - ACMソフトウェアシステム賞: 2013年 - ミシェル・モンペティ賞: 2015年 - 欧州アカデミー会員就任: 2014年
読者からの質問
### クリスティーヌ・ポーラン＝モーランの主な学術的焦点は何ですか？
彼女は対話型定理証明を専門とする数理論理学者であり計算機科学者です。
### 彼女が関わっている主要なソフトウェアシステムは何ですか？
彼女は、かつてCoqと呼ばれていたRocqとして知られる対話型定理証明器の研究で知られています。
.jpg)