| 研究課題/領域番号 |
16K00095
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| 研究協力者 |
田中 一成
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | 型システム / 中間言語 / 型検証 / プログラム検証 |
|---|
| 研究成果の概要 |
関数型プログラミング言語OCamlの型検証器の堅牢性を高めるために様々な研究に取り組んだ。型検証器の理論的な基盤の整理と型検証器の見通しの改善を目指し、まずGADT（一般化代数的データ型）のパターンマッチングの網羅性という問題に理論的に答えを与え、OCamlに反映させた。他の開発者とともに、型検証器のモジュール性を高めた。型付中間言語が安全性に効果的になるための条件も検討した。また、プログラムの形式的検証の様々な研究を通じて、今後の中間言語の形式化を準備した。
|
| 自由記述の分野 |
プログラミング言語の基礎理論
|
| 研究成果の学術的意義や社会的意義 |
社会のあらゆる所でソフトウェアは我々の生活をサポートしている。娯楽や書類の作成から、飛行機の飛行制御システムや医療機器まで、応用は幅広いが、その全ての場面で安全性が求められる。型システムがプログラムの安全性の確保に効果的であり、型の表現力が高いほどの効果が現れる。しかし、型システムが複雑になると、型の整合性の確認を行う型検証器とその後の処理の正しさの担保が難しくなる。この研究はプログラミング言語処理系の型の正しさを保証することでソフトウェアの安全性の向上を目指す。
|
