--- a/paper/introduction.tex	Thu Feb 09 18:58:53 2017 +0900
+++ b/paper/introduction.tex	Thu Feb 09 19:08:11 2017 +0900
@@ -30,11 +30,11 @@
 
 
 \section{本論文の構成}
-TODO: もう一回構成しなおし
 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
-CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。
+CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、GearsOS の解説を行なう。
+第\ref{chapter:akasha}章にて GearsOS 上の非破壊赤黒木の検証をメタ計算ライブラリ akasha にて行なう。
 次に第\ref{chapter:type}章で型システムについて取り上げる。
-型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。
+型システムの定義と CbC の型システムの定義に必要な単純型、レコード型、部分型について述べる。
 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。
 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。
 第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。