皆様（複数お受取になった場合はご容赦ください）， 東北大学の松田と申します．

来たる9月9日に開催される，日本ソフトウェア科学会第41回大会 (https://jssst2024.wordpress.com/) 併設イベント， PPLサマースクール2024「分離論理 Iris の世界」についてご案内いたします．

参加申し込みサイトはまだ準備中ですが近日中に下記リンク先にて公開予定です． https://jssst2024.wordpress.com/participation/

興味ある方は是非カレンダーに予定を入れておいていただけると幸いです．学 生は無料かつオンラインでも参加できますので是非参加を検討いただけばと存 じます．

（PPLサマースクールのみに参加する学生は参加申し込み窓口が異なる予定で す．ご注意ください）

==========

http://ppl.jssst.or.jp/index.php?ss2024

# PPLサマースクール2024「分離論理 Iris の世界」

日時：2024年9月9日(月) 13:00〜16:25 場所：立命館大学大阪いばらきキャンパスおよびオンラインのハイブリッド開催 講師：松下 祐介（京都大学 情報学研究科）

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

## 概要

プログラム検証における本質的な困難の一つが、メモリ上の可変オブジェクト に代表される、「可変状態」です。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 の研究に取り組んだ経験を踏まえて解説します。

## 参加費

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

## 問い合わせ先

PPLサマースクール2024 幹事 松田 一孝（東北大学） E-mail: [email protected]