| 研究概要 |
本研究が目的は,多相型理論やプログラムの論理学的基礎等の研究で蓄積された概念や方式を応用し,高い相互運用可能性(inter-operability),外部資源の柔軟で安全なアクセス,堅牢かつ効率良いコンパイル方式の特徴をあわせ持ったプログラミング言語を実現する理論的基礎を確立することである。
平成16年度は,以上の目的の下に,Krivine抽象機械の型理論とKrivine抽象機械へのコンパイル理論の構築を行った.Krivine抽象機械は,環境,Krivineスタック,ラムダ項からなる機械状態を変換する機械と見ることができる.環境は,通常の関数型言語の抽象機械と同様自由変数の値を保持する.Krivine抽象機械の最大の特徴は,環境に加えて,関数が使用される文脈を保持するKrivineスタックを用いる点にある.この機構により,関数の多重適用の際の不要なクロージャ生成が抑止され,関数型言語のより効率よいコードへのコンパイルが可能となる.Krivine抽象機械は,このように優れた特性を持つにも関わらず,その型の性質は解明されておらず,また,Krivine抽象機械コードへのコンパイルの型理論的性質も解明されていなかった.本研究では,これら2つの問題を共に解決し,Krivine抽象機械およびKrivine抽象機械コードへのコンパイルに対する型理論を確立した.これら成果は,2004年11月のプログラミング言語に関する国際会議(Asian Symposium on Programming Languages and Systems)にて発表した.以下の研究を実施した.
|
