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

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

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

# 研究内容(最近)
* Code Gear でプログラムを記述する理由に信頼性がある
* アルゴリズムそのものを証明してやることで信頼性を確保する
* Agda という証明支援系の言語に cbc を変換してやる

# 近況報告
* SingleLinkedStack の証明
    * 任意の数の要素を入れて同じだけ出すと
    * Stack は空になる
    * 順番は逆になってる
* 有限長の任意の要素が入る list を考える
    * (pop * n) (push * n) list == reverse list
    * push は a で pop は maybe a なのでlistが再構成できない


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