研究課題
この一年では、新たな型定義の形式化とその整合性のチェックを手がけた。しかし、定義される型が正則であることをチェックするアルゴリズムができたものの、その証明はまだ未完成である。この部分は今後もタリン工科大学の中田景子さんと協力して行う予定である。それ以外に、OCamlの現在の実装に関する改善や拡張も続けている。前年度に導入したGADT(一般化代数的データ型)の実装の強化や理論的な裏付けを行った。特に、フランスのINRIAのDidier Remyと一緒に考えた型推論の主要性を損なわないGADTの型システムを完全に形式化・証明し、2013年のAPLASで発表した。十分に形式化されたので、今後はCoqでの実装への導入も考えたい。もう一つの拡張はモジュールエイリアスの導入である。今まだは、OCamlで新しいモジュールを古いモジュールの別名として定義しても、型システムではモジュールの関係が分からなかった。そのせいで、型の等価性が不完全になったりした。また、効率の面でも、インターフェイスが無駄に大きくなったり、コンパイル時間にも影響していた。モジュールエイリアスの導入によって、そういう問題が解決できた。ちなみに、モジュールエイリアスの理論は中田景子さんと一緒に再帰モジュールのために作ったものであり、この先行研究がなければ理論的な難しさから実現しなかっただろう。こちらについては、部分的なCoqでの証明があるので、検証されたインタープリターでも導入を考える。
25年度が最終年度であるため、記入しない。
すべて 2014 2013 その他
すべて 雑誌論文 (2件) (うち査読あり 2件) 学会発表 (2件) 備考 (1件)
Mathematical Structures in Computer Science
巻: to appear ページ: to appear
APLAS 2013, Springer Verlag LNCS
巻: 2301 ページ: 257-272
10.1007/978-3-319-03542-0_19
http://www.math.nagoya-u.ac.jp/~garrigue/papers/aplas2010.html
