高機能高信頼多相型プログラミング言語の実現

点击翻译按钮获取中文摘要

本研究が目的は,多相型理論やプログラムの論理学的基礎等の研究で蓄積された概念や方式を応用し,高い相互運用可能性(inter-operability),外部資源の柔軟で安全なアクセス,堅牢かつ効率良いコンパイル方式の特徴をあわせ持ったプログラミング言語を実現する理論的基礎を確立することである.以上の目的の下に,平成15年度は,14年度の研究に引き続き,以下の研究を実施した.1.証明論に基づく新しいレジスタ割り付け方式の理論の完成とそのプロトタイプシステムの実装これは,従来のグラフ彩色に基づくレジスタ割り付けとは全く異なる,論理学的手法により,より堅牢で効率よいレジスタ割り付けを実現する方式である.これにより,レジスタ割り付け処理が型を保存する等の望ましい性質を簡単に証明可能になる.この成果は,プログラミング言語に関する主要な国際会議であるESOP 2003で発表した.2.証明論に基づくJAVAバイトコードのアクセス制御のための型システムの理論と実装これは,従来動的に行われているスタック検証と同等の効果を,コンパイル時に型システムによって行うことを可能にする新技術である.これにより,実行時のアクセス制御違反等が起りにくいより堅牢なシステムが実現可能となる.この成果は,プログラミング言語に関する主要な国際会議であるACM ICFP 2003で発表した.さらに,国際会議および研究集会にて,本研究成果に関する3件の招待講演を行った.