title: Type System of Continuation based C
author: Yasutaka Higa
profile:
lang: Japanese

# 研究目的
* 動作するプログラムの信頼性を保証したい
* 検証を行ないやすい単位としてプログラムをコードセグメントとデータセグメントという単位で記述する
* プログラムはコードセグメントという処理の集合として表され、相互に接続される
* 接続部分をメタ計算として定義し、その切り替えでプログラムの検証を行う

# 研究内容
* コードセグメントとデータセグメントを用いて記述する言語 Continuation based C に型を導入する
* CbCでは接続するコードセグメント群を元にデータセグメントを定義するためにプログラムの再利用性が高めづらい
* 型情報を用いてコードセグメントが接続可能かどうかをコンパイラやランタイムが判断できるようにする
* また、接続に必要なデータセグメントやスタブを自動生成する


# 近況報告
* Agda で stack の証明をちょっと書いたりしました
    * 任意の回数だけ push/pop を同じ回数行なうと同じものになる
* n 回pushとかを書いてる時に、CSの合成が書けないかと考えた
    * 引数が1つではないので無理
* 有限長の任意のtupleからtuple への function として定義できないかと考えた
    * 定義だけはできたが合成はできていない
* ゼミ前に okinawa/nakagusuku が調子悪くなったので資料はこれだけ(修復はしました)
* 修論の目次はマインドマップをちょっと書いたくらいです


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