--- a/paper/cbc-type.tex	Wed Feb 08 17:25:27 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 08 17:37:08 2017 +0900
@@ -3,13 +3,17 @@
 ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。
 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
 
+CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
+依存型を定義するためにもまず現状の CbC を型付けする必要がある。
+
 この章では CbC の型システムを部分型を利用して定義する。
-定義した型システムがきちんと検査されるかを確認するため、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、型付けされることを確認する。
-また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 証明する。
+定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
+また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。
 
 % {{{ 部分型付け
 
 \section{部分型付け}
+TODO: なおす
 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
 ここで、 単純型の拡張として、レコードを導入する。
 
@@ -511,7 +515,6 @@
 \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。
 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。
 
-% TODO  null check を入れる
 \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c}
 
 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。