2022 Fiscal Year Research-status Report
Type systems for verification of temporal and state-dependent properties in the presence of various computational effects
| Project/Area Number |
22K17875
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Keywords | プログラミング言語 / 型システム / 計算効果 / 時相的検証 |
|---|
| 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 |
今後の研究ではこれまでに構築した型理論を基にしたプログラム検証手法の実装や、状態に依存する性質を検証するための型理論の構築に取り組む。
|
| Causes of Carryover |
特に2022年度前半期において新型コロナウイルスの流行の継続により国内外の学会がオンラインでの開催となり、また研究出張や滞在も控えざるを得ない状況が続いたため。今後の使用計画としては、出張制限の緩和に伴う積極的な対外発表のための旅費や研究加速のための国際連携などへの使用を計画している。
|
Research Products
(6 results)
