| 研究課題/領域番号 |
21J14216
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 総合研究大学院大学 |
|---|
研究代表者 |
内藏 理史 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2021-04-28 – 2023-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
1,500千円 (直接経費: 1,500千円)
2021年度: 800千円 (直接経費: 800千円)
|
|---|
| キーワード | 圏論的意味論 / エフェクトハンドラー / プログラム検証 / Hoare論理 |
|---|
| 研究開始時の研究の概要 |
この研究で扱うのは検証，つまりプログラムの性質を数学的に保証する問題である．特に実際の開発現場でも使えるような実用的な検証にしたいという観点から，この研究では自動で検証ができる手法の獲得を目指す．さらに効率的な自動検証を行うために，「プログラム全体を一度に検証する代わりに，プログラムを構成する部品ごとに検証を行いそれらの結果をボトムアップにまとめていくことで全体としての検証ができる」という性質(合成性)を満たす手法を調べる．方針としては述語変換子やHoare論理といった検証の手法を圏論という数学の理論を用いて拡張して，得られた手法を自動検証器として実装することで新しい問題の検証へ適用する．
|
| 研究実績の概要 |
本年度は主にエフェクトハンドラーの検証のためのプログラム論理を圏論的意味論を用いて研究した．本研究のベースとなっているHermidaの研究ではfibrationと呼ばれるある種の関手に沿って単純型付きλ計算の意味論の"持ち上げ"を考えることでプログラムが満たす性質について議論するが，本研究ではエフェクトハンドラーの圏論的意味論として知られているEilenberg-Moore代数に対してある特定のfibrationに沿った持ち上げが存在するための十分条件を新たに与えた．さらに意味論側での持ち上げの存在の十分条件に対応するように構文側での十分条件を考えることで，エフェクトハンドラーの性質を証明するための推論規則を与えた．この推論規則は合成的であり，あるエフェクトハンドラーの性質の検証をそれぞれの代数的演算(algebraic operation)の性質の検証に帰着することができる．この推論規則を用いることでこれまで検証が難しかった，状態を扱うエフェクトハンドラーの検証が(現時点では非常に簡単なプログラムの例までしか考えていないものの)できるようになった．これらの研究成果は自身の博士論文の一つの章としてまとめた．また本研究成果の論文は近いうちに国際会議に投稿する予定である．
|
| 現在までの達成度 (段落) |
翌年度、交付申請を辞退するため、記入しない。
|
| 今後の研究の推進方策 |
翌年度、交付申請を辞退するため、記入しない。
|
