--- a/paper/atton-master.tex	Wed Feb 01 13:27:58 2017 +0900
+++ b/paper/atton-master.tex	Wed Feb 01 14:52:01 2017 +0900
@@ -116,9 +116,9 @@
 %chapters
 \input{introduction.tex}
 
-% \input{cbc.tex}
-% \input{type.tex}
-% \input{agda.tex}
+%\input{cbc.tex}
+%\input{type.tex}
+%\input{agda.tex}
 \input{cbc-type.tex}
 
 \chapter{まとめ}

--- a/paper/cbc-type.tex	Wed Feb 01 13:27:58 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 01 14:52:01 2017 +0900
@@ -1,11 +1,54 @@
 \chapter{Agda における Continuation based C の表現}
 \label{chapter:cbc-type}
+CbC の項を部分型を用いて Agda 上に記述していく。
+DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。
+また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。
+
+\section{DataSegment の定義}
+まず DataSegment から定義していく。
+DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。
+例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。
+cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。
+cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。
+
+\lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
+
 \section{CodeSegment の定義}
-\section{DataSegment の定義}
+次に CodeSegment を定義する。
+CodeSegment は DataSegment を取って DataSegment を返すものである。
+よって $ I \rightarrow O $ を内包するデータ型を定義する。
+
+レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。
+I は Input DataSegment の型であり、 O は  Output DataSegment である。
+
+CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。
+具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。
+
+\lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda}
+
+この CodeSegment 型を用いて CodeSegment の処理本体を記述する。
+
+まず計算の本体となる cs0 に注目する。
+cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。
+DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。
+そのレコードを引き連れたまま cs1 へと goto する。
+
+次に cs1 に注目する。
+cs1 は値に触れず cs2 へと goto するだけである。
+よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。
+
+最後に cs2 である。
+cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。
+どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。
+コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。
+
+最後に計算をする cs0 へと軽量継続する main を定義する。
+例として、 a の値を 100 とし、 b の値を50としている。
+正しく計算が行なえたら値150が得られるはずである。
+
 \section{ノーマルレベル計算の実行}
+\section{MetaDataSegment の定義}
 \section{MetaCodeSegment の定義}
-\section{MetaDataSegment の定義}
 \section{メタレベル計算の実行}
 \section{Agda を用いたContinuation based C の検証}
 \section{スタックの実装の検証}
-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/CodeSegment.agda	Wed Feb 01 14:52:01 2017 +0900
@@ -0,0 +1,14 @@
+data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where
+  cs : (I -> O) -> CodeSegment I O
+
+cs2 : CodeSegment ds1 ds1
+cs2 = cs id
+
+cs1 : CodeSegment ds1 ds1
+cs1 = cs (\d -> goto cs2 d)
+
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+main : ds1
+main = goto cs0 (record {a = 100 ; b = 50})

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/DataSegment.agda	Wed Feb 01 14:52:01 2017 +0900
@@ -0,0 +1,8 @@
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int