--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20140401/slide.md	Tue Apr 01 17:44:05 2014 +0900
@@ -0,0 +1,39 @@
+title: プログラムの静的解析による条件導出(仮)
+author: Yasutaka Higa
+cover:
+lang: Japanese
+
+
+# 研究目的(仮)
+
+* プログラムのデバッグは複雑になることがある
+* 例えば、あるif文の条件を満たすには、必要な状態がある
+* そういった状態を自動で導出したい
+* model checking を使えばいける?
+
+
+# 近況報告
+
+* 春休みの Haskell 勉強会 in ie
+* 研究室の大掃除
+* Existential on Agda
+
+
+# Existential on System F
+
+* 型変数を1つ持つ V において
+* 型 X と、型 V X である変数があれば Existential
+* つまり、 V には X を型変数として持つ型の変数が存在する、と
+* Existential であれば w が言える、というのは
+* 型 X と、型 V X である変数があれば w が導ける、と書ける
+* Existential から w が返ってくる、という式になる
+
+
+# Existential な例 (たぶんこんな感じ)
+
+* List a は 型変数 a を持つ V と言える
+* Existential Int, [1] とすれば、List には Int の要素が存在している、と
+* List a に対する演算があるとして、Existential があるのでそれは List Int に使えるよね、という形になる
+* そして、 List a の定義の a を Int に置換しても同じ、ということは保証されている
+
+<!-- vim: set filetype=markdown.slide: -->