研究課題
基盤研究(C)
関数型プログラミング言語OCamlの型検証器の堅牢性を高めるために様々な研究に取り組んだ。型検証器の理論的な基盤の整理と型検証器の見通しの改善を目指し、まずGADT（一般化代数的データ型）のパターンマッチングの網羅性という問題に理論的に答えを与え、OCamlに反映させた。他の開発者とともに、型検証器のモジュール性を高めた。型付中間言語が安全性に効果的になるための条件も検討した。また、プログラムの形式的検証の様々な研究を通じて、今後の中間言語の形式化を準備した。
社会のあらゆる所でソフトウェアは我々の生活をサポートしている。娯楽や書類の作成から、飛行機の飛行制御システムや医療機器まで、応用は幅広いが、その全ての場面で安全性が求められる。型システムがプログラムの安全性の確保に効果的であり、型の表現力が高いほどの効果が現れる。しかし、型システムが複雑になると、型の整合性の確認を行う型検証器とその後の処理の正しさの担保が難しくなる。この研究はプログラミング言語処理系の型の正しさを保証することでソフトウェアの安全性の向上を目指す。
すべて 2019 2018 2017 2016
すべて 雑誌論文 (3件) (うち国際共著 1件、 査読あり 3件、 オープンアクセス 3件、 謝辞記載あり 1件) 学会発表 (4件) (うち国際学会 1件)
Journal of Information Processing
巻: 印刷中
International Symposium on Information Theory and Its Applications, Singapore, October 28--31, 2018, IEICE/IEEE Xplore
巻: 1 ページ: 665-669
10.23919/isita.2018.8664276
Electronic Proceedings in Theoretical Computer Science
巻: 241 ページ: 23-35
10.4204/eptcs.241.2
