動的型付けと静的型付けを融合した漸進的型付けのメタ理論
| 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 |
Completed (Fiscal Year 2023)
|
| 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 |
当該年度は次の二つの課題について研究を進めた。
【多相性をもつ漸進的型付き言語】前年度までに引き続き、多相性を含む漸進的型付き言語の実装モデルである多相コアーション計算体系の空間効率性についての研究を行った。これまでの研究によりパラメトリシティと空間効率の良い多相コアーション計算は両立しないことがわかっていたが、本年度の研究により、一般的な多相計算体系における重要な性質であるパラメトリシティを一部あきらめる（具体的には動的型が型引数として使われた際にはパラメトリシティを保証しない）代わりに、多相コアーション計算体系を空間効率良く実装できることを証明した。本研究の成果により、多相性をサポートする漸進的型付け言語をより大規模なシステムに適用できる可能性を示すことができた。本成果はPLDI'24にて発表予定である。
【データ構造のための漸進的型付け】本年度は、前年度までに得られた知見を活用し、レコードなどのデータ構造操作を行うプログラミング言語のための漸進型付けの形式化および型システムにおける重要な性質である型健全性を証明した。本研究の成果により、漸進的型付けをデータ構造操作についても適用できることが示され、より多くのプログラムについて静的型付けと動的型付けを状況に応じて使い分けることが可能になると期待できる。今後は型健全性の他に、パラメトリシティといった重要な性質が成り立つことを確認後、国際会議への投稿を計画している。
|
Report
(5 results)
Research Products
(24 results)
