# HG changeset patch # User Yasutaka Higa # Date 1394519134 -32400 # Node ID d9592de1463960f3ededa1372e85811a06cc9403 # Parent 08d45d55313a76cb82933ff95023f80e69c11a46 Add slide for seminar diff -r 08d45d55313a -r d9592de14639 slides/20140311/slide.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/20140311/slide.md Tue Mar 11 15:25:34 2014 +0900 @@ -0,0 +1,18 @@ +title: プログラムから証明の自動生成(仮) +author: Yasutaka Higa +cover: +lang: Japanese + + +# 研究目的(仮) + +* プログラムの正しさを保証したい +* 既存のプログラムから証明支援系に変換できれば挙動を保証できる? +* 既存のプログラムのターゲットとしてはコードセグメントがある +* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する + +# 近況報告 + +* Proofs And Types 読み会 with 河野先生 + * Chapter 8 Coherence Space まで +* 猫番募集