changeset 41:15aba4b4c11f

Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 29 Apr 2014 17:42:46 +0900
parents 1419489ba107
children a10d98fd143f
files slides/20140429/slide.md
diffstat 1 files changed, 41 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /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: -->