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

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

本研究の目的は,多相型理論やプログラムの論理学的基礎等の研究で蓄積された概念や方式を応用し,高い相互運用可能性(inter-operability),外部資源の柔軟で安全なアクセス,堅牢かつ効率良いコンパイル方式の特徴をあわせ持ったプログラミング言語を実現する理論的基礎を確立することである.この目的の下に研究を行い以下のような成果をあげた.1.機械語コードのための証明論の完成.機械語コードをシーケント計算系の証明と解釈し,機械語コードの静的意味および動的意味の基礎を確立する研究を行い,機械語コードに対する型の導出は逐次シーケント計算系の証明に完全に対応し,さらに,機械語コードの実行は,逐次シーケント計算系の証明のCut除去定理に正確に対応することなどを主な内容とする機械語コードのための証明論を完成させ,この結果をまとめた論文T.Higuchi and A.Ohori, A Proof System for Machine Codeを完成させた.この論文は現在ACM Transactions on Programming Languages and Systemsに投稿中である.2.証明論に基づくJAVAバイトコードのアクセス制御のための型システムの理論の完成.従来動的に行われているスタック検証と同等の効果を,コンパイル時に型システムにょって行うことを可能にする新技術である.これまでに得られていた成果に,動的クラスローディングやオブジェクトの指定に関する種々の改良を加え,JAVAバイトコードのアクセス制御の理論を完成させた.この結果をまとめた論文は,平成17年11月にACM Transactions on Programming Languages and Systemsにaccept(採録決定)されている.