title: プログラムのデバッグ支援(仮)
author: Yasutaka Higa
cover:
lang: Japanese


# 研究目的(仮)

* プログラムのデバッグは複雑になることがある
* 例えば、あるif文の条件を満たすには、必要な状態がある
* そういった状態を自動で導出したい
* model checking を使えばいける?

# 近況報告

* 印鑑ください
* System F on Agda
    * List に手を出しました

# List on Agda

* List : X -> (U -> X -> X) -> X
* nil : List U
* nil = \x -> \y -> x
* cons : U -> List U -> List U
* cons u t = \x -> \y -> y u (t x y)

# 例としては

* u1,u2 : U
* cons u1 (cons u2 nil)
* X な x と (U -> X -> X) な f を渡すと
* f u1 (f u2 x)

# つまづいているところ

* t に nil と cons を渡せば t になる、というやつ
* U と List U を It するためにlevel は2つ
* でも合わない

<!-- vim: set filetype=markdown.slide: -->