--- a/paper/cbc-type.tex	Wed Feb 08 17:37:08 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 08 17:39:12 2017 +0900
@@ -4,9 +4,9 @@
 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
 
 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
-依存型を定義するためにもまず現状の CbC を型付けする必要がある。
+依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。
 
-この章では CbC の型システムを部分型を利用して定義する。
+~\ref{chapter:cbc-type}では CbC の型システムを部分型を利用して定義する。
 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。