annotate slides/20140325/slide.md @ 33:fb9d19430363

Add slides for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 25 Mar 2014 17:55:39 +0900
parents
children 8efe9eb8758b
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
33
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: 証明によるプログラムの信頼性の向上(仮)
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 cover:
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 # 研究目的(仮)
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * プログラムの正しさを保証したい
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * 既存のプログラムから証明支援系に変換できれば挙動を保証できる?
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 既存のプログラムのターゲットとしてはコードセグメントがある
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 * 挙動が保証されたプログラムの組み合せでプログラム全体を構成する
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 # 近況報告
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * Proofs and Types 読み会を河野先生とやってました
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * System F on Agda
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 * hg/Members/atton/agda/systemF にあります
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 * Boolean, Product, Sum まで書きました
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * Emp は放置
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * Existential は書いてみましたが黄色い
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
fb9d19430363 Add slides for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 <!-- vim : set filetype = markdown.slide -->