2023 Fiscal Year Research-status Report
| Project/Area Number |
19K20245
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| Project Period (FY) |
2019-04-01 – 2025-03-31
|
| Keywords | 定理証明支援系 / メタプログラミング |
|---|
| Outline of Annual Research Achievements |
2023年度は直接本課題の成果を外部に発表する機会はなかったが、いくつかの進捗が得られた。
メタプログラミングの側面としては、関数リアクティブプログラミング言語に対して時間の決定および分散システムへの応用を提案しているが、これをメタレベルの計算として行う仕組みについて検討している。
一方、検証の側面としては、データフロープログラミング言語に対する可逆計算のモデルとして作られた、部分関数を含むリスト計算についての定式化と、その無限リストへの展開を行っている。一般に無限リストは同一性を通常のリストのように行うことはできず、また定理証明支援系の体系では計算途中の失敗を全体の失敗とすることができない。これは、データフロープログラミング言語においてメタプログラミングを行うモジュールを無限に延長した場合に、大きな制限となることが予想される。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
メタレベルへの検証の適用が進んでおらず、検証システムの構築としては遅れている。
実際の検証を行うための情報は集まっているため、本年度の達成目標とする。
|
| Strategy for Future Research Activity |
定理証明支援系Coqを用い、簡易な言語によるメタレベルとベースレベルの実現、およびその上での検証を行う。
また、高階の検証が可能なライブラリIRISを用い、C言語を対象とした検証を試行する。
|
| Causes of Carryover |
コロナ禍以来、オンラインの参加を可能にしている学会も多く、加えて、今回は外部発表の機会もなかったため、参加における旅費の支出が抑えられていることが主な原因である。
2024年度の予算使用計画としては主に発表を行う国際学会への参加費および旅費、および論文掲載費、あわせて2,3回程度を想定している。
|
