Mercurial > hg > Members > atton > seminar_slides
view slides/20140325/slide.md @ 34:8efe9eb8758b
Update template
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 25 Mar 2014 18:38:04 +0900 |
parents | fb9d19430363 |
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 -->