title: プログラムのデバッグ支援(仮) author: Yasutaka Higa cover: lang: Japanese # 研究目的(仮) * プログラムのデバッグは複雑になることがある * 例えば、あるif文の条件を満たすには、必要な状態がある * そういった状態を自動で導出したい * model checking を使えばいける? # 近況報告 * インストール大会 * Int in Agda # Int in Agda * だいたい Church 数な感じ * Int : X -> (X -> X) -> X * O : Int * O = \x -> \f -> x * S : Int -> Int * S t = \x -> \f -> f (t) * 定義はしたけれど命題はちょっと詰まってます