研究課題
若手研究(B)
ヒープに割り当てられたデータ構造の書き換えを含むプログラムの変換方法についての研究を行った。このようなプログラムはポインタの操作を直接的に扱わなければならないが、ポインタ操作を含むプログラムの変換はそうでないものの変換よりも格段に難しく、その変換手法については系統的なものはあまり知られていなかった。本年度の研究では、形式的技法の分野で研究されてきているプログラムの詳細化の手法を、ポインタやヒープに関する性質を記述するための論理体系のひとつであるSeparation Logicで拡張した。これによって、プログラム中のポインタ操作がすべて、Separation Logicにおける中核的な2種類の論理演算と対応するふたつの一般化されたポインタ操作の組み合わせで表せることが明らかとなった。これら二つの操作に関する変換規則を整備して適用することにより、ポインタ操作を含むプログラムの系統的な変換手法への糸口を見出した。またこの内容を定理証明系の上で実装し、これを用いて正しさの保証されたポインタ操作を含むプログラムの変換を行うことができることを示した。これらの結果は、いくつかの国内の研究集会で発表され、また2008年7月にフランスで開催される国際会議Mathematics of Program Construction(MPC'08)でも発表予定である。また、勝股審也氏との共同研究による、モノイド準同型を用いた代数的手法に基づいた累積変数を持つ関数プログラムの融合変換手法についての共著論文が著名雑誌Journal of Functional Programmingに近日掲載されることが決定した。この論文は2006年に国際会議ICFP'06において発表したものを拡張しまとめたものである。
すべて 2009 2008 2007 2006
すべて 雑誌論文 (4件) (うち査読あり 1件) 学会発表 (3件)
Journal of Functional Programming (2009年以降掲載予定)
Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006 LNCS 4019
ページ: 293-307
ICFP'06: Proceedings of the 11th ACMSIGPLAN International Conference on Functional Programming
ページ: 227-238
SPACE 2006 : Third workshop on semantics, program analysis and computing evironements for memory management (unofficial proceedings)
ページ: 101-104
