# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1397552137 -32400
# Node ID 1fde03546bbc1db06a0dde5934d2814c33c18eb3
# Parent  c7d57cf16fdb83494742d47a89f8289058502517
Add slide for seminar

diff -r c7d57cf16fdb -r 1fde03546bbc slides/20140415/slide.md
--- /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: -->