\chapter{まとめ}
本論文ではメタ計算を用いた Continuation based C プログラムの検証手法を二つ提案した。

一つはモデル検査的なアプローチであり、メタ計算ライブラリ akasha を用いて GearsOS の非破壊赤黒木の仕様を保証した。
CbC における仕様の定義は assert に渡す論理式として定義され、状態の数え上げは軽量継続 \verb/meta/ を切り替えることで実現できた。
CbC で記述された非破壊赤黒木のプログラムを検証用に変更することなく、CbC 自身で検証した。
検証できた範囲は有限の要素数のみであるが、有限モデルチェッカ CBMC よりも大きな範囲を検証した。

二つめは定理証明的なアプローチである。
akasha を用いた検証では挿入回数は有限の数に限定されていた。
プログラムを直接証明することにより、任意の回数の操作においても性質を保証する。
部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。
Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。

また、型システムは証明以外にも実用的に利用できることが分かった。
akasha を用いて検証を行なう際、全ての CodeSegment に対して stub をユーザが定義する必要があった。
CbC の型を定義することにより、stub の自動生成と型チェックが行なえることが分かった。

\section{今後の課題}
今後の課題として、型システムの詳細な性質の解析がある。
本論文では部分型の定義を CbC に適用した。
CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。
その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。

また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。
加えて部分型を組み込むことにより、stub の自動生成ができる。
さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。
他にも SingleLinkedStack の証明を元にした赤黒木の証明などが考えられる。

モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。

また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。
多相型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
他にも、CbC の型推論や推論器の実装などが挙げられる。