Mercurial > hg > Members > atton > seminar_slides
changeset 35:196a6a236f41
Add slide for seminar
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 01 Apr 2014 17:44:05 +0900 |
parents | 8efe9eb8758b |
children | 32cbe5f209f1 |
files | slides/20140401/slide.md |
diffstat | 1 files changed, 39 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /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: -->