| 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 |
Sekiyama Taro 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (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 Final Research Achievements |
This research aims to "advance the theory of gradual typing" and "explore the limitation of gradual typing." To this end, we focused on parametric polymorphism, a type-based mechanism to enhance the reuse of program components. In particular, we studied (1) a relationship between parametric polymorphism and space-efficiency, (2) a relationship between parametric polymorphism and data structures, and (3) a relationship between parametric polymorphism and computational effects. The results we obtained can be summarized as follows: (1) We proved that there is a trade-off between parametric polymorphism and space-efficiency in gradual typing. (2) We successfully introduced extensible data structures and row polymorphism into gradual typing. (3) We successfully provided novel polymorphic type systems for algebraic effect handlers, a programming mechanism to implement various computational effects in a programmable manner.
|
| Academic Significance and Societal Importance of the Research Achievements |
漸進的型付けは動的・静的型付けの長所を臨機応変に使い分けることのできる新たな型付け方式で、TypeScriptをはじめ、様々なプログラミング言語で実用化されている。一方漸進的型付けによって保証される性質を理論的に解析することは、漸進的型付けの有用性を明らかにする上で重要である。本研究の目的は「漸進的型付けの更なる発展」と「漸進的型付けの限界を探る」ための理論研究を推進することである。またこれらの研究を通じ、将来的に「漸進的型付けの核はどこにあるのか」という根源的かつメタ的な問いを明らかにし、漸進的型付けの研究を正しい方向に加速させ、その抜本的な改革につながることを目指す。
|
