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: -->