| 研究課題/領域番号 |
22K17875
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| キーワード | プログラミング言語 / 型システム / 計算効果 / 時相的検証 |
|---|
| 研究実績の概要 |
2022年度は限定継続演算子を利用するプログラムの時相的性質を検証するための手法について研究を行った。限定継続演算子は限定継続と呼ばれる、一種のプログラム文脈を値として取り出すことのできる命令で、これを利用することで例外、バックトラック、ジェネレーターなどの、計算効果を引き起こす様々なプログラミング機能が実装できることが知られている。そのためこの命令を扱えるような検証手法を与えることで、上記に挙げたプログラミング機能を利用するプログラムの性質を検証することが可能となる。2022年度はshift0/resetと呼ばれる限定継続演算子に対し、時相的性質を検証するための型理論を構築し、検証手法実装への足がかりを掴んだ。
また今回の手法を応用することで、エフェクトハンドラと呼ばれる別種の限定継続演算子に対して依存篩型による正確な検証を可能にする型理論を構築することにも成功した。
さらに限定演算子の利用を前提とした時相的検証の研究を通して、より一般的な再帰型を用いるプログラムを対象とした時相的検証に関する知見を得ることができた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
本年度では当初の計画通り、限定継続演算子を対象とした時相的性質の検証のための型理論が構築できた。またその際のアイディアが、時相的検証のみならず篩型によるプログラムの正確な安全性検証にも利用できる点、さらにはより一般的な再帰型を利用するプログラムに対する時相的検証を行うための知見を得た点は、当初想定していた以上の進展である。
|
| 今後の研究の推進方策 |
今後の研究ではこれまでに構築した型理論を基にしたプログラム検証手法の実装や、状態に依存する性質を検証するための型理論の構築に取り組む。
|
| 次年度使用額が生じた理由 |
特に2022年度前半期において新型コロナウイルスの流行の継続により国内外の学会がオンラインでの開催となり、また研究出張や滞在も控えざるを得ない状況が続いたため。今後の使用計画としては、出張制限の緩和に伴う積極的な対外発表のための旅費や研究加速のための国際連携などへの使用を計画している。
|
