| 研究概要 |
本研究では,オブジェクト指向プログラミング言語のための,再利用性の向上をサポートする型システム技術を確立することを目指している.本年度の研究成果は以下のとおりである.
1.入れ子構造を導入したオブジェクト指向言語の意味論と型理論
昨年度までの研究成果である,入れ子構造を導入した言語の型理論variant path typesを実際の言語に対して適用するための課題として残されていた,型検査アルゴリズムの構築とその正しさの証明を行った.これにより,与えられたプログラムが型付けできるかどうかを自動的に判定できるようになる.
2.軽量族多相の型理論的分析
これまでに研究成果である拡張可能な相互再帰的クラス定義を支援するための軽量族多相機構をJava5などに見られる総称クラスとF-bounded多相の機構に帰着させた.具体的には,軽量族多相のモデルである.FJから,総称クラスのモデルであるFeatherweight GJへの変換を定義し,変換が型付けと操作的意味を保存することを証明した.この結果,Java 5の機能だけでは忠実に帰着できないことがわかり,それを補完するための型付け機構を考案した.この研究により,軽量族多相機構の多くの部分が,従来から研究されてきた型理論により説明可能になるとともに,軽量族多相の本質的な利点が明らかになった.
|
