動的型付けと静的型付けを融合した漸進的型付けのメタ理論
Project/Area Number |
19K20247
|
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) |
2019-04-01 – 2024-03-31
|
Project Status |
Granted (Fiscal Year 2022)
|
Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2021: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
Keywords | プログラミング言語 / 漸進的型付け / 多相性 / 型システム / 継続渡し形式 / 漸進的型システム / 計算効果 |
Outline of Research at the Start |
ソフトウェアを検証するために広く使用されている方法として型システムがある。型システムは実行前に検証を行う静的型付けと実行時に検証を行う動的型付けに大別することができ、それぞれ相補的な長所と短所をもつ。 本研究ではこれら二つの異なる型付けを組み合わせ、両者の長所を活かすことのできる、漸進的型付けと呼ばれるソフトウェア検証手法に関する研究を行う。本研究では特に漸進的型付き言語の正しい設計方針と漸進的型付けの理論的限界を与える漸進的型付けのメタ理論について研究を行い、漸進的型付け理論の研究を正しく加速させ、高生産・高信頼なソフトウェア開発を実現することを目指す。
|
Outline of Annual Research Achievements |
【多相性をもつ漸進的型付き言語】前年度までに引き続き、多相性を含む漸進的型付き言語の実装モデルである多相コアーション計算体系の、特に空間効率についての理論研究を行った。これまでの研究成果で多相性における重要な性質であるパラメトリシティと空間効率の良い実装が両立しないことは判明していたが、本年度は新たにその原因が名前生成の機構にあることを理論的に示した。また逆に、パラメトリシティを(完全にではないが)ある程度あきらめることで、多相性を含む漸進的型付き言語を空間的に効率良く実装するための知見を得た。
【データ構造のための漸進的型付け】これまでにも様々なデータ構造を扱うために、列多相性をサポートする漸進的型付き言語の研究に取り組んできた。しかしこれまで考えていた列多相性はフィールド名の重複を許すものであったため、型上で表現された列構造の動的検査のための仕組みが想定以上に複雑になってしまっていた。そこで本年度では重複を許さない列多相を対象とした漸進的型付き言語の設計を行った。その結果、実行検査の仕組みが簡便になる見通しを得た。
|
Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
多相性のための漸進的型付けに対しては、パラメトリシティを犠牲にすることで空間効率の良い実装を行う算段を得ることができた。これは当初想定していなかった成果である。一方データ構造を扱うための漸進的型付き言語については当初計画していたよりも設計や理論構築に遅れが生じている。以上を総合的に考え、順調に進展していると判断した。
|
Strategy for Future Research Activity |
2022年度は当研究課題を遂行する上での重要な知見を得ることができたため、今後はそれらを基にした型理論の構築や構築した理論の解析、ならびに論文執筆に取り組む。
|
Report
(4 results)
Research Products
(20 results)