Mercurial > hg > Members > atton > seminar_slides
changeset 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 | cc91543302b3 |
children | 8efe9eb8758b |
files | slides/20140325/slide.md |
diffstat | 1 files changed, 22 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/20140325/slide.md Tue Mar 25 17:55:39 2014 +0900 @@ -0,0 +1,22 @@ +title: 証明によるプログラムの信頼性の向上(仮) +author: Yasutaka Higa +cover: +lang: Japanese + +# 研究目的(仮) + +* プログラムの正しさを保証したい +* 既存のプログラムから証明支援系に変換できれば挙動を保証できる? +* 既存のプログラムのターゲットとしてはコードセグメントがある +* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する + +# 近況報告 + +* Proofs and Types 読み会を河野先生とやってました +* System F on Agda + * hg/Members/atton/agda/systemF にあります + * Boolean, Product, Sum まで書きました + * Emp は放置 + * Existential は書いてみましたが黄色い + +<!-- vim : set filetype = markdown.slide -->