view slides/20140311/slide.md @ 31:d9592de14639

Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 11 Mar 2014 15:25:34 +0900
parents
children
line wrap: on
line source

title: プログラムから証明の自動生成(仮)
author: Yasutaka Higa
cover:
lang: Japanese


# 研究目的(仮)

* プログラムの正しさを保証したい
* 既存のプログラムから証明支援系に変換できれば挙動を保証できる?
* 既存のプログラムのターゲットとしてはコードセグメントがある
* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する

# 近況報告

* Proofs And Types 読み会 with 河野先生
    * Chapter 8 Coherence Space まで
* 猫番募集