PPLサマースクール2024
「分離論理 Iris の世界」
 
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第41回大会 併設企画
 
講師：松下 祐介（京都大学 情報学研究科）
 
2024年9月9日(月) 13:00〜16:25
立命館大学大阪いばらきキャンパスおよびオンラインのハイブリッド開催
 

ニュース †

↑

参加者向け情報 †

PPLサマースクール2024は対面を中心としたハイブリッド形式で開催いたします．大会自体は対面のみの開催であることにご注意ください．

  • Zoomでのオンライン配信を行う予定です．
  • 対面・オンライン参加者用の非同期的な質疑・交流の場（SlackあるいはDiscord等）を提供予定です．
↑

概要 †

プログラム検証における本質的な困難の一つが、メモリ上の可変オブジェクトに代表される、「可変状態」です。2001年に O'Hearn らが築いた「分離論理」は、論理式に所有権を持たせるというアイデアで、可変状態についてのスケーラブルな推論を実現しました。分離論理はプログラム検証における一大分野として非常に活発に研究されています。特に、並行計算への拡張「並行分離論理」は2016年に Gödel 賞を受賞しました。 そうした中で特に注目されているのが、2015年に Jung らが開発した高階並行分離論理フレームワーク「Iris」https://iris-project.org/ です。Iris は多くの推論機構を包摂する、拡張性の高い汎用分離論理フレームワークであり、定理証明支援系 Coq 上の成熟したライブラリとして機械化されています。Rust の所有権型システムを検証した2018年 Jung らの「RustBelt?」を筆頭に、ここ数年 Iris を用いる論文がPL系トップ国際会議に多数採択されており、2023年には Iris の功績に Church 賞が与えられました。

この講義では、実際に Iris を使う研究に取り組む松下氏を講師としてお招きし、分離論理の初歩からはじめて、現代的な分離論理の基礎、Iris の発展的話題、Iris の Rust への応用といったトピックについて解説いただきます。

↑

講師紹介 †

松下 祐介（京都大学 情報学研究科）

現在 京都大学大学院 情報学研究科 五十嵐・末永研究室 特定研究員 (学振PD)。2024年 東京大学大学院 情報理工学系研究科 コンピュータ科学専攻 博士課程修了 (指導教員: 小林直樹 教授)、博士 (情報理工学)。2019年 東京大学 理学部情報科学科 卒業。 Rust プログラムを「預言」の手法でステートレスな表現に帰着して自動検証する「RustHorn?」(松下ら、ESOP '20・TOPLAS '21) が代表作。RustHorn? 流帰着の正しさを分離論理 Iris で証明する、ドイツ MPI-SWS RustBelt?/Iris チームとの共同研究「RustHornBelt?」(松下ら、PLDI '22) 、Iris の鍵となる高階幽霊状態という機能における later 様相の問題を解決する研究「Nola」(松下、博論 '24) など、分離論理 Iris を使う研究にも従事。

↑

プログラム †

13:00 - 13:05オープニング
13:05 - 14:05現代的な分離論理の基礎
14:05 - 14:25休憩
14:25 - 15:25Iris の発展的話題
15:25 - 15:45休憩
15:45 - 16:45Iris × Rust

現代的な分離論理の基礎
2001年に生まれた分離論理は、現代にいたるまでの20数年で急速に発展しています。この部では、分離論理の初歩からはじめて、Iris による高度な拡張にいたるまで、現代的な分離論理の基礎を解説します。

Iris の発展的話題
この部では、Iris の発展的な話題について説明します。
Iris で鍵となる仕組みである「高階幽霊状態」、これを扱うための「later 様相」や「step-indexing」といった機能について説明します。これに関連して、講師の博士論文の成果となった研究「Nola」についても話します。
また、Iris が Coq ライブラリとしてどのような設計になっているか、Iris を使ってどのように可変状態を扱う検証プロジェクトを Coq で機械化できるかについても説明します。

Iris × Rust
Iris の重要な応用例の一つが、2015年に生まれたプログラミング言語「Rust」の所有権型についての検証です。2018年の Jung らによる「RustBelt?」は、Rust で鍵となる仕組みである「借用」を Iris でモデル化し、Rust のメモリ・スレッド安全性保証を検証しました。2022年の松下らによる「RustHornBelt?」は、RustBelt? を拡張し、RustHorn? 流の帰着の正しさを一般に証明しました。
この部では、こうした Iris の Rust への応用について、実際に RustHornBelt? の研究に取り組んだ経験を踏まえて解説します。

↑

参加費・参加申し込み †

PPLサマースクールの参加費は以下の通りです．

  • 一般会員：1000円
  • 一般非会員：2000円
  • 学生会員, 学生非会員：無料

日本ソフトウェア科学会第41回大会 参加申し込みページから申し込みください．立命館大学の学生，それ以外の学生でPPLサマースクールのみ申し込む場合，それ以外の方で申し込みフォームが分かれておりますのでご注意ください．

↑

問い合わせ先 †

PPLサマースクール2024 幹事
松田 一孝（東北大学）
E-mail: kztk[at]tohoku.ac.jp

↑

過去のサマースクール †