2013 Fiscal Year Annual Research Report
進んだ型システムを持ったプログラミング言語における型検証器の機械的な証明
| Project/Area Number |
22700028
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2010-04-01 – 2014-03-31
|
| Keywords | 型推論 / アルゴリズムの証明 / モジュール / 交際情報交換 |
|---|
| Research Abstract |
この一年では、新たな型定義の形式化とその整合性のチェックを手がけた。しかし、定義される型が正則であることをチェックするアルゴリズムができたものの、その証明はまだ未完成である。この部分は今後もタリン工科大学の中田景子さんと協力して行う予定である。
それ以外に、OCamlの現在の実装に関する改善や拡張も続けている。前年度に導入したGADT(一般化代数的データ型)の実装の強化や理論的な裏付けを行った。特に、フランスのINRIAのDidier Remyと一緒に考えた型推論の主要性を損なわないGADTの型システムを完全に形式化・証明し、2013年のAPLASで発表した。十分に形式化されたので、今後はCoqでの実装への導入も考えたい。
もう一つの拡張はモジュールエイリアスの導入である。今まだは、OCamlで新しいモジュールを古いモジュールの別名として定義しても、型システムではモジュールの関係が分からなかった。そのせいで、型の等価性が不完全になったりした。また、効率の面でも、インターフェイスが無駄に大きくなったり、コンパイル時間にも影響していた。モジュールエイリアスの導入によって、そういう問題が解決できた。ちなみに、モジュールエイリアスの理論は中田景子さんと一緒に再帰モジュールのために作ったものであり、この先行研究がなければ理論的な難しさから実現しなかっただろう。こちらについては、部分的なCoqでの証明があるので、検証されたインタープリターでも導入を考える。
|
| Current Status of Research Progress |
Reason
25年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
25年度が最終年度であるため、記入しない。
|
