Mercurial > hg > Members > atton > seminar_slides

comparison slides/20140401/slide.md @ 35:196a6a236f41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 01 Apr 2014 17:44:05 +0900
parents
children
comparison
equal deleted inserted replaced
34:8efe9eb8758b 35:196a6a236f41
1 title: プログラムの静的解析による条件導出(仮)
2 author: Yasutaka Higa
3 cover:
4 lang: Japanese
5
6
7 # 研究目的(仮)
8
9 * プログラムのデバッグは複雑になることがある
10 * 例えば、あるif文の条件を満たすには、必要な状態がある
11 * そういった状態を自動で導出したい
12 * model checking を使えばいける?
13
14
15 # 近況報告
16
17 * 春休みの Haskell 勉強会 in ie
18 * 研究室の大掃除
19 * Existential on Agda
20
21
22 # Existential on System F
23
24 * 型変数を1つ持つ V において
25 * 型 X と、型 V X である変数があれば Existential
26 * つまり、 V には X を型変数として持つ型の変数が存在する、と
27 * Existential であれば w が言える、というのは
28 * 型 X と、型 V X である変数があれば w が導ける、と書ける
29 * Existential から w が返ってくる、という式になる
30
31
32 # Existential な例 (たぶんこんな感じ)
33
34 * List a は 型変数 a を持つ V と言える
35 * Existential Int, [1] とすれば、List には Int の要素が存在している、と
36 * List a に対する演算があるとして、Existential があるのでそれは List Int に使えるよね、という形になる
37 * そして、 List a の定義の a を Int に置換しても同じ、ということは保証されている
38
39 <!-- vim: set filetype=markdown.slide: -->