表現力が高く安全に相互運用可能なプログラミング言語の理論と実現

2012 Fiscal Year Annual Research Report

• Project/Area Number: 10J06019
• Research Institution: Kyoto University
• Principal Investigator: 伊奈 林太郎 京都大学, 大学院・情報学研究科, 特別研究員(DC1)
• Keywords: プログラミング言語 / 安全性 / 型理論 / 動的型 / 相互運用 / 停止性

Research Abstract

[研究目的]
ソフトウェアプログラムは,安全に実行できる信頼性が要求される一方で,コストを抑えるために迅速かつ柔軟に開発する必要がある.前者の実現のために,型理論の成果を用いた静的型付け言語がプログラミング言語として広く用いられている一方,後者を優先する場合は動的型付け言語が用いられる場合が多く,どちらを用いるかは開発を開始する段階で決めねばならず,途中で変更することができない.そこで本研究では,柔軟な開発を可能にする動的型付け言語の特性と,安全性を保証する静的型付け言語の特性を併せ持ち,これらの特性を開発の段階やソフトウェアプログラムの部位によって使い分けることができる言語を提案する.これにより,柔軟かつ安全なソフトウェアプログラムの開発が可能となる.
[研究成果]
前年度までに,Javaを拡張し静的型付けと動的型付けを混在できる言語のための数学的なモデルが得られていたが,実際の処理系を実装するためのアルゴリズムの一部が欠けていた.具体的には,より詳細な型がよりおおまかな型に含まれることを表す部分型という関係を検査する必要があり,前年度までに提案した手続きではジェネリクスを含む場合に停止することが示せていなかった.本年度はこの手続きの停止性を証明することに成功し,部分型検査のためのアルゴリズムを完成させることができた.この成果については前年度までの成果とともに雑誌論文として発表する予定である.また,ジェネリクスを含まない簡略化された言語に関しての実装も進めた.