| 研究概要 |
多相型レコード計算の理論やデータベースの多相型理論などを基礎とし,・高機能多相型システム,・高い相互運用可能性(inter-operability),・外部資源の柔軟で安全なアクセス,・堅牢かつ効率良い実装 の特徴をあわせ持つ,広域分散環境に適した新しいプログラミング言語の実現を目指した研究を行い,以下の成果をあげた.
(1)相互運用のための型理論の構築
レコード多相性の理論を基礎とし,ML系言語からJAVA等のオブジェクト指向言語のクラスを透明に使用可能にする理論を構築し,そのプロトタイプを実装した.
(2)証明論に基づくJAVAバイトコードの検証の理論
JAVAのバイトコードを,論理学の証明とみなすことにより,その整合性を自動検証する理論を構築し,そのプロトタイプを実装した.
(3)レジスタ割り付けの理論的基礎
証明論的考え方を用いて,正しさが検証可能でかつより系統的なレジスタ割り当て方式の理論を構築し,そのプロトタイプを実装した.
(1)と(2)の成果は,2002年10月のACM主催のプログラミング言語に関するの国際会議にて発表した.(3)の成果は2003年4月ETAPS主催のプログラミング言語に関するの国際会議にて発表予定である.
|
