| 研究課題/領域番号 |
19K20247
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2021年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2020年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2019年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 漸進的型付け / プログラミング言語 / 型システム / 多相性 / 計算効果 / レコード / 継続渡し形式 / 漸進的型システム |
|---|
| 研究開始時の研究の概要 |
ソフトウェアを検証するために広く使用されている方法として型システムがある。型システムは実行前に検証を行う静的型付けと実行時に検証を行う動的型付けに大別することができ、それぞれ相補的な長所と短所をもつ。
本研究ではこれら二つの異なる型付けを組み合わせ、両者の長所を活かすことのできる、漸進的型付けと呼ばれるソフトウェア検証手法に関する研究を行う。本研究では特に漸進的型付き言語の正しい設計方針と漸進的型付けの理論的限界を与える漸進的型付けのメタ理論について研究を行い、漸進的型付け理論の研究を正しく加速させ、高生産・高信頼なソフトウェア開発を実現することを目指す。
|
| 研究成果の概要 |
本研究では「漸進的型付けの更なる理論的発展」と「漸進的型付けの限界を探る」ため、パラメリック多相性（以下、単に多相性と呼ぶ）と呼ばれる、型に基づくプログラム部品の再利用機構に着目した。特に(1)多相性と空間効率性の関係、(2)多相性とデータ構造の関係、(3)多相性と計算効果の関係について研究を行った。その結果、(1)漸進的型付けでは多相性と空間効率性にはトレードオフがあることを証明、(2)拡張可能なデータ構造と列多相の漸進的型付けへの導入に成功、(3)多様な計算効果を実現するためのプログラミング機構である代数的エフェクトハンドラに対し、新たな多相型システムの構築に成功、という成果が得られた。
|
| 研究成果の学術的意義や社会的意義 |
漸進的型付けは動的・静的型付けの長所を臨機応変に使い分けることのできる新たな型付け方式で、TypeScriptをはじめ、様々なプログラミング言語で実用化されている。一方漸進的型付けによって保証される性質を理論的に解析することは、漸進的型付けの有用性を明らかにする上で重要である。本研究の目的は「漸進的型付けの更なる発展」と「漸進的型付けの限界を探る」ための理論研究を推進することである。またこれらの研究を通じ、将来的に「漸進的型付けの核はどこにあるのか」という根源的かつメタ的な問いを明らかにし、漸進的型付けの研究を正しい方向に加速させ、その抜本的な改革につながることを目指す。
|
