| 研究概要 |
1.多相型(総称型)・抽象型(存在型)および再帰型をもつλ計算での双模倣について、国際論文誌Journal of the ACMに論文を投稿し、採録・掲載された。この結果により、モジュールやオブジェクト、多相関数やジェネリックス、ループや再帰関数などのある、従来よりも現実的なプログラミング言語におけるプログラム等価性証明が可能となった。
2.種々の高階プログラミング言語モデル(λ計算および高階II算)のための双模倣(プログラム等価性の証明手法)について、国際会議IE EE LICS 2007にて発表した。特にup-to techniquesと呼ばれる補助手法により、以前の双模倣より容易にプログラムの等価性が証明できるようになった。
3.C言語のポインタ演算を安全なJava言語へ変換する手法についての論文誌論文を投稿し、採録された。fat pointer, fat integerおよびアクセスメソッドと呼ばれる仕組みにより、ポインタと整数のキャストにも対応しつつ、比較的単純なベンチマークにおいては、各種最適化により元々のCプログラムの1.3〜5.9倍程度の実行時間を達成した。
|
