view slides/20140311/slide.md @ 158:6e4a6421f168

Fix slide
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 13 Dec 2016 19:48:44 +0900
parents d9592de14639
children
line wrap: on
line source

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


# 研究目的(仮)

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

# 近況報告

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