Mercurial > hg > Members > atton > generated_seminar_slides
changeset 10:e01286cc7696
auto-Update generated slides by script
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 25 Mar 2014 17:45:20 +0900 |
parents | 80c6faf18967 |
children | 3fe5bd1b1793 |
files | slides/20140325/slide.md |
diffstat | 1 files changed, 21 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:45:20 2014 +0900 @@ -0,0 +1,21 @@ +<!-- vim : set filetype = markdown.slide --> +title: 証明によるプログラムの信頼性の向上(仮) +author: Yasutaka Higa +cover: +lang: Japanese + +# 研究目的(仮) + +* プログラムの正しさを保証したい +* 既存のプログラムから証明支援系に変換できれば挙動を保証できる? +* 既存のプログラムのターゲットとしてはコードセグメントがある +* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する + +# 近況報告 + +* Proofs and Types 読み会を河野先生とやってました +* System F on Agda + * hg/Members/atton/agda/systemF にあります + * Boolean, Product, Sum まで書きました + * Emp は放置 + * Existential は黄色い