| Project/Area Number |
22K17875
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2024: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2023: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2022: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | プログラミング言語 / 型システム / 計算効果 / 時相的検証 / 形式検証 |
|---|
| Outline of Research at the Start |
高信頼ソフトウェアの実現には状態管理が必要な様々な機能群（計算効果）に対応したプログラム検証技術が必要となる．本研究課題では計算効果の正しい使い方を表わす時相的性質と，プログラムの状態に関する状態依存的性質を検証するための新たな型システムについて研究を行う．これらの性質を検証することで，プログラムが計算効果を正しく使用しているか，プログラムが計算効果の正しい状態を保持しているかが検証可能となる．
|
| Outline of Annual Research Achievements |
2022年度は限定継続演算子を利用するプログラムの時相的性質を検証するための手法について研究を行った。限定継続演算子は限定継続と呼ばれる、一種のプログラム文脈を値として取り出すことのできる命令で、これを利用することで例外、バックトラック、ジェネレーターなどの、計算効果を引き起こす様々なプログラミング機能が実装できることが知られている。そのためこの命令を扱えるような検証手法を与えることで、上記に挙げたプログラミング機能を利用するプログラムの性質を検証することが可能となる。2022年度はshift0/resetと呼ばれる限定継続演算子に対し、時相的性質を検証するための型理論を構築し、検証手法実装への足がかりを掴んだ。
また今回の手法を応用することで、エフェクトハンドラと呼ばれる別種の限定継続演算子に対して依存篩型による正確な検証を可能にする型理論を構築することにも成功した。
さらに限定演算子の利用を前提とした時相的検証の研究を通して、より一般的な再帰型を用いるプログラムを対象とした時相的検証に関する知見を得ることができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
本年度では当初の計画通り、限定継続演算子を対象とした時相的性質の検証のための型理論が構築できた。またその際のアイディアが、時相的検証のみならず篩型によるプログラムの正確な安全性検証にも利用できる点、さらにはより一般的な再帰型を利用するプログラムに対する時相的検証を行うための知見を得た点は、当初想定していた以上の進展である。
|
| Strategy for Future Research Activity |
今後の研究ではこれまでに構築した型理論を基にしたプログラム検証手法の実装や、状態に依存する性質を検証するための型理論の構築に取り組む。
|
