# HG changeset patch # User Yasutaka Higa # Date 1395737120 -32400 # Node ID e01286cc769638faf0f504c654a6c11d92676168 # Parent 80c6faf18967be19bee651848a81602603fc9593 auto-Update generated slides by script diff -r 80c6faf18967 -r e01286cc7696 slides/20140325/slide.md --- /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 @@ + +title: 証明によるプログラムの信頼性の向上(仮) +author: Yasutaka Higa +cover: +lang: Japanese + +# 研究目的(仮) + +* プログラムの正しさを保証したい +* 既存のプログラムから証明支援系に変換できれば挙動を保証できる? +* 既存のプログラムのターゲットとしてはコードセグメントがある +* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する + +# 近況報告 + +* Proofs and Types 読み会を河野先生とやってました +* System F on Agda + * hg/Members/atton/agda/systemF にあります + * Boolean, Product, Sum まで書きました + * Emp は放置 + * Existential は黄色い