| 研究課題/領域番号 |
17H01723
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究分担者 |
馬谷 誠二 神奈川大学, 理学部, 准教授 (40378831)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
18,720千円 (直接経費: 14,400千円、間接経費: 4,320千円)
2019年度: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2018年度: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2017年度: 5,850千円 (直接経費: 4,500千円、間接経費: 1,350千円)
|
|---|
| キーワード | 漸進的型付け / プログラミング言語 / 型システム / 計算効果 / 顕在的契約計算 / 非決定計算 / トレース意味論 |
|---|
| 研究成果の概要 |
漸進的型付けはひとつのプログラム中に静的型付けされる部分と動的型付けされる部分を共存させるための、プログラミング言語技術である．これを先進的なプログラミング言語に適用するための理論的基盤の研究を行った．主な成果は、多相性、セッション型、篩型、非決定性、ML型推論、交差型といった先進的なプログラミング言語機構へ漸進的型付けを導入した計算体系を与え、その性質(型安全性など)を証明した．さらに、漸進的型付けの実装技術として提案されている空間効率のよいコアーション計算を改良し、コアーション渡し形式を経由するコンパイル方法を提案し、実際に実装・評価を行い、その効果を確認した．
|
| 研究成果の学術的意義や社会的意義 |
漸進的型付けの概念は、JavaScript に静的型を導入した TypeScript の登場などにより、現実のプログラミング言語にも適用され始めているが、先進的な型機構とどう共存できるか明らかではなく、また実行時オーバーヘッドが大きいことが本格的な導入の障壁になっていた．本研究成果は、漸進的型付けを先進的なプログラミング言語に導入するための理論的な基盤を整備するものであると同時に、効率的な実行を可能とするコンパイル手法の理論の改良を提案するとともに、実装を通じてその効果を評価したものである．
|
