# HG changeset patch # User Yasutaka Higa # Date 1395737739 -32400 # Node ID fb9d19430363eaa9909b59b40118ee679bec4cde # Parent cc91543302b31894375fdc37c4c64e47f952d1a3 Add slides for seminar diff -r cc91543302b3 -r fb9d19430363 slides/20140325/slide.md --- /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 は書いてみましたが黄色い + +