非述語的多相型付けを用いたプログラム融合変換

ヒープに割り当てられたデータ構造の書き換えを含むプログラムの変換方法についての研究を行った。このようなプログラムはポインタの操作を直接的に扱わなければならないが、ポインタ操作を含むプログラムの変換はそうでないものの変換よりも格段に難しく、その変換手法については系統的なものはあまり知られていなかった。本年度の研究では、形式的技法の分野で研究されてきているプログラムの詳細化の手法を、ポインタやヒープに関する性質を記述するための論理体系のひとつであるSeparation Logicで拡張した。これによって、プログラム中のポインタ操作がすべて、Separation Logicにおける中核的な2種類の論理演算と対応するふたつの一般化されたポインタ操作の組み合わせで表せることが明らかとなった。これら二つの操作に関する変換規則を整備して適用することにより、ポインタ操作を含むプログラムの系統的な変換手法への糸口を見出した。またこの内容を定理証明系の上で実装し、これを用いて正しさの保証されたポインタ操作を含むプログラムの変換を行うことができることを示した。これらの結果は、いくつかの国内の研究集会で発表され、また2008年7月にフランスで開催される国際会議Mathematics of Program Construction(MPC'08)でも発表予定である。また、勝股審也氏との共同研究による、モノイド準同型を用いた代数的手法に基づいた累積変数を持つ関数プログラムの融合変換手法についての共著論文が著名雑誌Journal of Functional Programmingに近日掲載されることが決定した。この論文は2006年に国際会議ICFP'06において発表したものを拡張しまとめたものである。

ヒープに割り当てられたデータ構造の書き換えを含むプログラムの変換方法についての研究を行った。このようなプログラムはポインタの操作を直接的に扱わなければならないが、ポインタ操作を含むプログラムの変換はそうでないものの変換よりも格段に難しく、その変換手法については系統的なものはあまり知られていなかった。本年度の研究では、形式的技法の分野で研究されてきているプログラムの詳細化の手法を、ポインタやヒープに関する性質を記述するための論理体系のひとつであるSeparation Logicで拡張した。これによって、プログラム中のポインタ操作がすべて、Separation Logicにおける中核的な2種類の論理演算と対応するふたつの一般化されたポインタ操作の組み合わせで表せることが明らかとなった。これら二つの操作に関する変換規則を整備して適用することにより、ポインタ操作を含むプログラムの系統的な変換手法への糸口を見出した。またこの内容を定理証明系の上で実装し、これを用いて正しさの保証されたポインタ操作を含むプログラムの変換を行うことができることを示した。これらの結果は、いくつかの国内の研究集会で発表され、また2008年7月にフランスで開催される国際会議Mathematics of Program Construction(MPC'08)でも発表予定である。また、勝股審也氏との共同研究による、モノイド準同型を用いた代数的手法に基づいた累積変数を持つ関数プログラムの融合変換手法についての共著論文が著名雑誌Journal of Functional Programmingに近日掲載されることが決定した。この論文は2006年に国際会議ICFP'06において発表したものを拡張しまとめたものである。