\chapter{ラムダ計算と型システム}
\label{chapter:type}
\ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
CbC は直接自身を証明する機構が存在しない。
プログラムの性質を証明するには CbC の形式的な定義が必須となる。
\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。


\section{型システムとは}
\section{型なしラムダ計算}
\section{単純型付きラムダ計算}
\section{部分型付け}
\section{部分型と Continuation based C}