| Project/Area Number |
21J14216
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
内藏 理史 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2021-04-28 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 2021: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | 圏論的意味論 / エフェクトハンドラー / プログラム検証 / Hoare論理 |
|---|
| Outline of Research at the Start |
この研究で扱うのは検証，つまりプログラムの性質を数学的に保証する問題である．特に実際の開発現場でも使えるような実用的な検証にしたいという観点から，この研究では自動で検証ができる手法の獲得を目指す．さらに効率的な自動検証を行うために，「プログラム全体を一度に検証する代わりに，プログラムを構成する部品ごとに検証を行いそれらの結果をボトムアップにまとめていくことで全体としての検証ができる」という性質(合成性)を満たす手法を調べる．方針としては述語変換子やHoare論理といった検証の手法を圏論という数学の理論を用いて拡張して，得られた手法を自動検証器として実装することで新しい問題の検証へ適用する．
|
| Outline of Annual Research Achievements |
本年度は主にエフェクトハンドラーの検証のためのプログラム論理を圏論的意味論を用いて研究した．本研究のベースとなっているHermidaの研究ではfibrationと呼ばれるある種の関手に沿って単純型付きλ計算の意味論の"持ち上げ"を考えることでプログラムが満たす性質について議論するが，本研究ではエフェクトハンドラーの圏論的意味論として知られているEilenberg-Moore代数に対してある特定のfibrationに沿った持ち上げが存在するための十分条件を新たに与えた．さらに意味論側での持ち上げの存在の十分条件に対応するように構文側での十分条件を考えることで，エフェクトハンドラーの性質を証明するための推論規則を与えた．この推論規則は合成的であり，あるエフェクトハンドラーの性質の検証をそれぞれの代数的演算(algebraic operation)の性質の検証に帰着することができる．この推論規則を用いることでこれまで検証が難しかった，状態を扱うエフェクトハンドラーの検証が(現時点では非常に簡単なプログラムの例までしか考えていないものの)できるようになった．これらの研究成果は自身の博士論文の一つの章としてまとめた．また本研究成果の論文は近いうちに国際会議に投稿する予定である．
|
| Research Progress Status |
翌年度、交付申請を辞退するため、記入しない。
|
| Strategy for Future Research Activity |
翌年度、交付申請を辞退するため、記入しない。
|
