Mercurial > hg > Members > atton > seminar_slides
view slides/20140325/slide.md @ 163:b8e16c48a5a4 default tip
Update template
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 17 Jan 2017 17:18:41 +0900 |
parents | 8efe9eb8758b |
children |
line wrap: on
line source
title: プログラムから証明の自動生成(仮) author: Yasutaka Higa cover: lang: Japanese # 研究目的(仮) * プログラムの正しさを保証したい * 既存のプログラムから証明支援系に変換できれば挙動を保証できる? * 既存のプログラムのターゲットとしてはコードセグメントがある * 挙動が保証されたプログラムの組み合せでプログラム全体を構成する # 近況報告 * Proofs and Types 読み会を河野先生とやってました * System F on Agda * hg/Members/atton/agda/systemF にあります * Boolean, Product, Sum まで書きました * Emp は放置 * Existential は書いてみましたが黄色い <!-- vim : set filetype = markdown.slide -->