|
研究代表者の提案した双模倣による文脈等価性の証明手法を、より広範な言語に適用できるように一般化した。具体的には、(1)もっとも基本的な計算モデルの一つである、副作用のない名前呼びλ計算(2)破壊的代入と参照(reference)のある値呼びλ計算(3)コードを値として送受信できる並行計算のモデルである高階π計算の3つについて、研究代表者の方法が適用できることを確認した。
さらに、"up-to techniques"と呼ばれる複数の補助技法を提案した。特に、"up-to context"という補助技法より、高階関数について必要だった複雑な条件を単純化した。
以上の成果を、理論計算機科学においてもっとも著名な国際会議の一つであるIEEE Symposium on Logic in Computer Science(LICS2007)に投稿し、受理・発表が決定している。
並行して、抽象型を暗号化によって実装し、型検査されていない攻撃者からも情報を保護する通信ライブラリQuicksilver/O Camlをプログラミング言語Objective Camlにおいて実現した。具体的には、抽象型の値がモジュールから出ていくときに暗号化し、戻ってくるときに復号化する、という処理を実装した。暗号化・復号化を行う関数の組を型の表現とするテクニックにより、Objective Camlを変更せずライブラリとして実現することができた。
この成果は、日本ソフトウェア科学会 第9回プログラミングおよびプログラミング言語ワークショップ(PPL2007)に投稿・受理され、発表された。
また、安全でないプログラミング言語Cを(互換性を損なわず)安全なプログラミング言語Javaに変換する研究についても、同ワークショップに投稿・受理・発表された。
|
