| 研究課題/領域番号 |
19K20245
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2025-03-31
|
| キーワード | 定理証明支援系 / メタプログラミング |
|---|
| 研究実績の概要 |
2023年度は直接本課題の成果を外部に発表する機会はなかったが、いくつかの進捗が得られた。
メタプログラミングの側面としては、関数リアクティブプログラミング言語に対して時間の決定および分散システムへの応用を提案しているが、これをメタレベルの計算として行う仕組みについて検討している。
一方、検証の側面としては、データフロープログラミング言語に対する可逆計算のモデルとして作られた、部分関数を含むリスト計算についての定式化と、その無限リストへの展開を行っている。一般に無限リストは同一性を通常のリストのように行うことはできず、また定理証明支援系の体系では計算途中の失敗を全体の失敗とすることができない。これは、データフロープログラミング言語においてメタプログラミングを行うモジュールを無限に延長した場合に、大きな制限となることが予想される。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
メタレベルへの検証の適用が進んでおらず、検証システムの構築としては遅れている。
実際の検証を行うための情報は集まっているため、本年度の達成目標とする。
|
| 今後の研究の推進方策 |
定理証明支援系Coqを用い、簡易な言語によるメタレベルとベースレベルの実現、およびその上での検証を行う。
また、高階の検証が可能なライブラリIRISを用い、C言語を対象とした検証を試行する。
|
| 次年度使用額が生じた理由 |
コロナ禍以来、オンラインの参加を可能にしている学会も多く、加えて、今回は外部発表の機会もなかったため、参加における旅費の支出が抑えられていることが主な原因である。
2024年度の予算使用計画としては主に発表を行う国際学会への参加費および旅費、および論文掲載費、あわせて2,3回程度を想定している。
|
