PPLサマースクール2024
「分離論理 Iris の世界」
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第41回大会 併設企画
講師：松下 祐介（京都大学 情報学研究科）
2024年9月9日(月) 13:00〜16:25
立命館大学大阪いばらきキャンパスおよびオンラインのハイブリッド開催
ニュース
- [2025-01-09] スライドは https://shiatsumat.github.io/talks/ppl-ss-2024-iris-lecture.pdf から入手可能です．
- [2025-01-09] 講演の録画 https://youtu.be/uqZEJv9wvBA を公開しました．
参加者向け情報
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:25 | Iris の発展的話題 |
| 15:25 - 15:45 | 休憩 |
| 15:45 - 16:45 | Iris × 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
過去のサマースクール
- 第6回 PPLサマースクール (PPL Summer School 2008)
今日から使える! みんなの静的解析・バグ検出ツール - 第8回 PPLサマースクール (PPL Summer School 2010)
マルチコア時代の新言語 - 第9回 PPLサマースクール (PPL Summer School 2011)
クラウドのプログラミング - 第10回 PPLサマースクール (PPL Summer School 2012)
関数型言語ベースの先進的Webフレームワーク - 第11回 PPLサマースクール (PPL Summer School 2013)
高階モデル検査とその応用 - 第12回 PPLサマースクール (PPL Summer School 2014)
高性能計算のプログラミングの最前線 - 第13回 PPLサマースクール (PPL Summer School 2015)
プログラミング言語のゲーム意味論 - 第14回 PPLサマースクール (PPL Summer School 2016)
商用Java処理系の研究開発 - 第15回 PPLサマースクール (PPL Summer School 2017)
Isabelle/HOL による証明とプログラミング - 第16回 PPLサマースクール (PPL Summer School 2018)
SML#コンパイラを使いこなす - 第17回 PPLサマースクール (PPL Summer School 2019)
ブロックチェーンと形式検証 - 第18回 PPLサマースクール (PPL Summer School 2021)
JavaScript処理系とChromeブラウザの実装技術 - 第19回 PPLサマースクール (PPL Summer School 2022)
計算効果入門 — プログラミングから理論まで — - 第20回 PPLサマースクール (PPL Summer School 2023)
正規表現研究の最先端