--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20140415/slide.md	Tue Apr 15 17:55:37 2014 +0900
@@ -0,0 +1,41 @@
+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: -->