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

Research Project

Project/Area Number	16016240
Research Category	Grant-in-Aid for Scientific Research on Priority Areas
Allocation Type	Single-year Grants
Review Section	Science and Engineering
Research Institution	Tohoku University (2005) Japan Advanced Institute of Science and Technology (2004)
Principal Investigator	大堀淳東北大学, 電気通信研究所, 教授 (60252532)
Project Period (FY)	2004 – 2005
Project Status	Completed (Fiscal Year 2005)
Budget Amount *help	¥6,400,000 (Direct Cost: ¥6,400,000) Fiscal Year 2005: ¥3,300,000 (Direct Cost: ¥3,300,000) Fiscal Year 2004: ¥3,100,000 (Direct Cost: ¥3,100,000)
Keywords	プログラミング言語 / 型理論 / コンパイラ / メモリー管理 / 多相型システム / Krivine型システム / バイトコード / 型主導コンパイル
Research Abstract	本研究の目的は,多相型理論やプログラムの論理学的基礎等の研究で蓄積された概念や方式を応用し,高い相互運用可能性(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(採録決定)されている.