--- a/paper/cbc-type.tex	Fri Feb 03 11:59:41 2017 +0900
+++ b/paper/cbc-type.tex	Fri Feb 03 14:49:58 2017 +0900
@@ -171,7 +171,10 @@
 
 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda}
 
-メタの階層構造を表すと図のようになる。
+なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる
+% TODO: cbc と agda の diff
+
+CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。
 Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。
 
 
@@ -179,5 +182,27 @@
 
 % }}}
 
-\section{Agda を用いたContinuation based C の検証}
+\section{Agda を用いた Continuation based C の検証}
+Agda において CbC の CodeSegment と DataSegment を定義することができた。
+実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
+
+ここでは赤黒木の実装に用いられているスタックの性質について注目する。
+この時のスタックはポインタを利用した片方向リストを用いる。
+
+CbC における構造体 \verb/stack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。
+
+\lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h}
+
+Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。
+CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定して、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。
+
+\verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。
+片方のコンストラクタ \verb/just/ は値を持つ。
+これは計算を行なうことができる値であり、ポインタの先に値があることに対応している。
+一方のコンストラツア \verb/nothing/ は値を持たない。
+これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。
+
+\lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced}
+
+
 \section{スタックの実装の検証}