title: Verification method of programs using Continuation based C
author: Yasutaka Higa
profile:
lang: Japanese

# 研究目的
* 動作するプログラムの信頼性を保証したい
* 検証を行ないやすい単位としてプログラムをコードセグメントとデータセグメントという単位で記述する
* プログラムはコードセグメントという処理の集合として表され、相互に接続される
* 型検査器を導入することでコードセグメントが接続可能かどうかを判断する
* また、コードセグメントの型から推論してデータセグメントの生成を行なう

# 研究内容
* コードセグメントとデータセグメントを用いて記述する言語 Continuation based C に型を導入する
* コードセグメント内部の演算と変数代入から型を推論する
* 接続可能かどうかをコンパイル時に判断し、必要なデータセグメントを型情報から生成する


# 近況報告
* Gears の Stack の証明をこねてました
    * 任意の Stack に対して n回 push した後に n回 pop したら元に戻る
    * 空の Stack に対しても同様
* Gears の型をどうするかのアイデア

# Type of Gears
* CodeSegment のは DataSegment -> DataSegment
    * DataSegment は制約か部分型
    * 合成できるのならOK
* 全ての部分型を満たすものが最初の引数になるのでそれを生成できれば良い
* 関数合成部分を切り替え可能なメタ計算にする
    * Allocate とかも書けそう

# 問題点
* どう書くか/書けるのか
* goto の分岐
* 総称型に拡張可能かどうか
* 並列実行はどう書くのか
    * まだAPIが無い


<!-- vim: set filetype=markdown.slide: -->