2018 Fiscal Year Annual Research Report
Game semantics and intersection type systems for program verification
| Project/Area Number |
16K16004
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | プログラム意味論 / ゲーム意味論 / 交差型システム / generalised species / 線形論理 |
|---|
| Outline of Annual Research Achievements |
本研究は関数型プログラミング言語のモデルであるλ計算について「ゲーム意味論と交差型システムの対応関係」を確立し、得られた知見を基に並行計算のモデルであるπ計算の交差型システムを設計した上で検証等へ応用するものであった。
(1) λ計算のモデルについて、前年度に得られた結果をさらに発展させ、非決定性プログラム・確率的プログラム・量子的プログラムなどを一様に扱うことのできる意味論の枠組みを与えることに成功した。この枠組は、通常の交差型システムの一般化であること理解することができ、「型が付くか否か」という質的な情報だけではなく、「どの程度型が付くのか」という量的な情報を扱うことができるものである。量的な情報を交差型システムを利用して記述する手法については多くの先行研究があるが、本成果は扱える量的な情報のクラスを非常に一般的な代数構造に拡張したことが新しい。本結果はトップ国際会議である Logic in Computer Science に採録された。
(2) π計算のための交差型システムについては、前年度までに技術的な課題が明らかになっていた。本年度は、技術的困難の詳細な調査と解決を目指し、π計算の理論を代数的観点から見直す研究を行った。成果は国際会議 European Symposium on Programming に再録された。本結果が明らかにしたことは、π計算は線形論理という論理体系の特殊な形であると理解できるこいうことである。線形論理と交差型システムの関連は良く知られており、本結果はπ計算の交差型システムへの指針を与えることが期待できる。
|
