2006-11-29 PLAN-X 2007 研究 受理されたようです．発表するのは共著者の予定． 前の日記でも少し触れたが，最近Coqにハマっている． とりあえずtree transducer関連のものを片っ端から定式化しているけども， まだgoal-directedの証明に慣れてない所為かcut規則を使いまくっている． 知らない戦略が多いのでかなり無駄なことをやってる気がするが， Proof completedが出た時の達成感はこの上ない．
