Theory and Application for Robust and High-Performance Systems Programming Languages

点击翻译按钮获取中文摘要

トップ国際会議 ACM PLDI 2022 に前年度に条件付きで採択された主著論文 "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code"（松下、Denis、Jourdan、Dreyer）について、論文およびアーティファクト（ソースコード等）の最終版を提出し、論文の最終的な採択・アーティファクトの再利用可能性評価を得て、正式に出版した。さらに、論文の上位約1割にのみ与えられる Distinguished Paper Award を受賞した。この論文は、RustHorn（松下ら、2020）で提案された、Rust の所有権型と預言（未来の情報の先取り）の手法を利用して Rust プログラムを効率よく検証する手法の正当性を、様々な API を含む Rust の広いサブセットに対し一般に証明するための枠組みを提案し、定理証明支援系 Coq と分離論理フレームワーク Iris で機械化して実証した、というものである。そして、アメリカ・サンディエゴで開催された国際会議 ACM PLDI 2022 に現地参加し、コロナ禍で長らく難しかった世界の研究者たちとの対面による密な交流を果たし、主著論文 "RustHornBelt" について口頭で発表・議論した。また、世界の最新の研究動向について知見を得て、自分の研究についても知ってもらえるように働きかけた。東京大学大学院理学系研究科・理学部ニュース 2022年5月号 の「理学のススメ」に単著で一般向けの研究紹介記事「ソフトウェアの世界を切り拓く」を寄稿した。この記事では、研究分野の背景、研究という営みに対して抱いている思い、RustHorn のアイデアなどについて書いている。