2018 Fiscal Year Annual Research Report
Design of a typed intermediate language for a richly typed programming language
| Project/Area Number |
16K00095
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 型システム / 中間言語 / 型検証 / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
昨年に続き、今後のOCamlの発展に合ったデザインを検討した。フロントエンド(パーザや前処理および型推論)とバックエンド(コードの生成・変換と最適化)が常に発展を続けており、全てを同時に変更するのが難しい。対応策として、OCamlのモジュールシステムを活用し、型抽象によって各部の独立性を高めた上で部分的な変換を段階的に導入する方針を固めた。
また、それと平行して、型システムの様々なバグを直した。特に再帰モジュールとファンクター(モジュール間の関数)や実モジュールの抽象化から得られたシグネチャー(モジュールの型)の組み合わせにより健全でないモジュールが前から作れていたことが発覚し、その問題の理解を深めながら理論と実装を修正した。同様にクラスの全称化のときに起きていた健全性の問題を修正した。健全性の問題が実際に実行時の型の不整合により未定義な動作を許してしまうので、その修正は重要だが、それを未然に防げる方法の必要性が再確認できた。
OCaml自体を一つの中間言語とみなすこともできる。岐阜大学の今井敬吾と一緒に、OCamlでの線形型やセッション型のエンコーディングを提唱した。型システムを拡張するのではなく、現在の型システムとモナドなどを使い、値が線形的に使われることが保証できる。
プログラム検証の面で、産業技術総合研究所のReynald Affeldtや学生の田中一成とQi Xuanruiと一緒に簡潔データ構造の木を扱ういくつかのアルゴリズムの検証を行った。簡潔データ構造は大量のデータを復号化なしでコンパクトに表現できるこてで、大量のデータを扱うときに役に立つが、安全性も求められる。検証はCoqで行ったが、今後はOCamlでコンパイルされたコードとCoqで証明されたプログラムの関係を証明できり方法を確率して、実行されるコードまでが保証される機構を目指したい。
|
