# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1398760966 -32400
# Node ID 15aba4b4c11faeba8967f12537052ea7397bfcb4
# Parent  1419489ba1072e141431b969abc92f13bb61429d
Add slide for seminar

diff -r 1419489ba107 -r 15aba4b4c11f slides/20140429/slide.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20140429/slide.md	Tue Apr 29 17:42:46 2014 +0900
@@ -0,0 +1,41 @@
+title: プログラムのデバッグ支援(仮)
+author: Yasutaka Higa
+cover:
+lang: Japanese
+
+
+# 研究目的(仮)
+
+* プログラムのデバッグは複雑になることがある
+* 例えば、あるif文の条件を満たすには、必要な状態がある
+* そういった状態を自動で導出したい
+* 証明とかすれば良い？
+
+# 近況報告
+
+* Proofs and Types
+    * Curry Howard Isomorphism of System F
+    * cut elimination
+* Integer on Agda
+    * add とか書いてみてます
+    * R を使うと割と上手くいってません
+
+
+# Integer on Agda
+
+* Int から Int を作成する場合、使い方によっては作成した Int の型が確定されてしまう
+* 一旦lambdaで受けるという手
+    * kono先生の source はそんな感じ
+* R を使うと lambda で受けるとかでなく確定されちゃう?
+    * R を2回使って add を定義してみたは良いものの……
+    * 黄色い
+    * R に product が入ってるのは関係ありそう？
+
+# Product on Agda
+* R に Product が使われてるのは関係あったりしない？
+* < π1 < u , v >  , π2 < u , v > > ≡ < u , v >
+* が通らないのは書かれてるのではともかく
+* < u , v > ≡ < u , v >
+* すら黄色い……
+
+<!-- vim: set filetype=markdown.slide: -->