|
平成25年度は、設計中の汎用性の高い型付中間言語の特色のうち、高速な多次元配列操作のための型検査方式の検討を中心に進めた。例えば、科学技術計算を行うアプリケーションを高水準言語で作成する場合などにおいては、しばしば多次元配列を使用したいことがある。そのような言語から安全な型付中間言語に翻訳する処理系を考える。高速な多次元配列操作のためには、添字計算のコストとともに、実行時境界チェックのコストをできるだけ省きたい。一般に型付中間言語においては、値に関する情報などを型レベルで表現できるような依存型を用いることにより、後続の命令において不要なチェックなどを省く機会が得られる。そこで、依存型で用いるための多次元配列向けの述語を検討した。
研究期間全体として本研究は、仮想機械のRISC 化を目標に型システムを構築することで、安全性を維持しつつビットレベル構造を扱う命令への型付けを含む圧倒的な自由度(汎用性) と高速性を持つ型付中間言語（以降、この言語を"MIL" と呼ぶ）を設計しようとするものであった。MIL の特色のうち、ビットレベル表現のサポートでは、場合依存型という新しい概念と、BDD (二分決定グラフ) を用いた命令列の妥当性確認の枠組みに関して研究を進めた。Lisp 系言語などで使われるfixnum などのサポートが場合分けを利用して行われるようになることを確認しつつ、応用を拡大することを目指して、特に、シフト命令への対応について考察した。また、MIL の特色のうち、オブジェクトの初期化（特に循環参照）のサポートでは、provisional assumptions という新しい概念と依存型による命令列の妥当性確認の枠組みに関して研究を進めた。最後に、正確なごみ集めのサポートが最も挑戦的な課題であったが、課題の整理を進めるにとどまったため今後の課題としたい。
|
