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

Research Project

Project/Area Number	14019043
Research Category	Grant-in-Aid for Scientific Research on Priority Areas
Allocation Type	Single-year Grants
Review Section	Science and Engineering
Research Institution	Japan Advanced Institute of Science and Technology
Principal Investigator	大堀淳北陸先端科学技術大学院大学, 情報科学研究科, 教授 (60252532)
Project Period (FY)	2002
Project Status	Completed (Fiscal Year 2002)
Budget Amount *help	¥5,400,000 (Direct Cost: ¥5,400,000) Fiscal Year 2002: ¥5,400,000 (Direct Cost: ¥5,400,000)
Keywords	プログラミング言語 / コンパイラ / 型理論 / ソフトウエア学 / 計算機システム
Research Abstract	多相型レコード計算の理論やデータベースの多相型理論などを基礎とし,・高機能多相型システム,・高い相互運用可能性(inter-operability),・外部資源の柔軟で安全なアクセス,・堅牢かつ効率良い実装の特徴をあわせ持つ,広域分散環境に適した新しいプログラミング言語の実現を目指した研究を行い,以下の成果をあげた. (1)相互運用のための型理論の構築レコード多相性の理論を基礎とし,ML系言語からJAVA等のオブジェクト指向言語のクラスを透明に使用可能にする理論を構築し,そのプロトタイプを実装した. (2)証明論に基づくJAVAバイトコードの検証の理論 JAVAのバイトコードを,論理学の証明とみなすことにより,その整合性を自動検証する理論を構築し,そのプロトタイプを実装した. (3)レジスタ割り付けの理論的基礎証明論的考え方を用いて,正しさが検証可能でかつより系統的なレジスタ割り当て方式の理論を構築し,そのプロトタイプを実装した. (1)と(2)の成果は,2002年10月のACM主催のプログラミング言語に関するの国際会議にて発表した.(3)の成果は2003年4月ETAPS主催のプログラミング言語に関するの国際会議にて発表予定である.