Theory of Gradual Typing for Modern Programming Languages
| Project/Area Number |
17H01723
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
馬谷 誠二 神奈川大学, 理学部, 准教授 (40378831)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥18,720,000 (Direct Cost: ¥14,400,000、Indirect Cost: ¥4,320,000)
Fiscal Year 2019: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2018: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2017: ¥5,850,000 (Direct Cost: ¥4,500,000、Indirect Cost: ¥1,350,000)
|
|---|
| Keywords | 漸進的型付け / プログラミング言語 / 型システム / 計算効果 / 顕在的契約計算 / 非決定計算 / トレース意味論 |
|---|
| Outline of Final Research Achievements |
Gradual typing is a programming-language technique that allows statically typed and dynamically typed parts to coexist in a single program. We have studied the theoretical foundations for applying this technique to advanced programming languages. The main result is computational calculi that introduce gradual typing to advanced programming language mechanisms such as polymorphism, session types, refinement types, nondeterminism, ML type inference, and intersection types; we have proved its properties (such as type safety). In addition, we improved space-efficient coercions that have been proposed as an implementation technique for gradual typing by coercion passing style compilation, which we implemented and evaluated.
|
| Academic Significance and Societal Importance of the Research Achievements |
漸進的型付けの概念は、JavaScript に静的型を導入した TypeScript の登場などにより、現実のプログラミング言語にも適用され始めているが、先進的な型機構とどう共存できるか明らかではなく、また実行時オーバーヘッドが大きいことが本格的な導入の障壁になっていた．本研究成果は、漸進的型付けを先進的なプログラミング言語に導入するための理論的な基盤を整備するものであると同時に、効率的な実行を可能とするコンパイル手法の理論の改良を提案するとともに、実装を通じてその効果を評価したものである．
|
Report
(4 results)
Research Products
(57 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Gradual Session Types2017
Author(s)
Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, Philip Wadler
-
Journal Title
Proceedings of the ACM on Programming Languages
Volume: 1 Issue ICFP
Issue: ICFP
Pages: 1-28
DOI
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] Gradual Session Types2017
Author(s)
Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, Philip Wadler
Organizer
ACM SIGPLAN International Conference on Functional Programming
Related Report
Int'l Joint Research
-
