--- a/paper/atton-master.tex	Mon Jan 16 15:47:43 2017 +0900
+++ b/paper/atton-master.tex	Mon Jan 16 16:28:42 2017 +0900
@@ -90,13 +90,44 @@
 \mainmatter
 
 %chapters
-% \input{intro.tex}
-% \input{cerium.tex}
-% \input{cbc.tex}
-% \input{gearsos.tex}
-% \input{comparison.tex}
-% \input{evaluation.tex}
-% \input{conclusion.tex}
+\chapter{Continuation based C とメタ計算としての検証手法}
+
+\chapter{Continuation based C}
+\section{CodeSegment と DataSegment}
+\section{Continuation based C における CodeSegment と DataSegment}
+\section{MetaCodeSegment と MetaDataSegment}
+\section{GearsOS}
+
+\chapter{ラムダ計算と型システム}
+\section{型システムとは}
+\section{型なしラムダ計算}
+\section{単純型付きラムダ計算}
+\section{部分型付け}
+\section{部分型と Continuation based C}
+
+\chapter{証明支援系言語 Agda による証明手法}
+\section{TODO: Agda tutorial 的なもの}
+\section{Natural Deduction}
+\section{Curry-Howard Isomorphism}
+\section{Reasoning}
+
+\chapter{Agda における Continuation based C の表現}
+\section{CodeSegment の定義}
+\section{DataSegment の定義}
+\section{ノーマルレベル計算の実行}
+\section{MetaCodeSegment の定義}
+\section{MetaDataSegment の定義}
+\section{メタレベル計算の実行}
+
+\chapter{Continuation based C の検証}
+\section{証明を用いた検証}
+\section{スタックの実装の検証}
+\section{メタ計算を用いた検証}
+\section{メタ計算ライブラリ akasha}
+\section{赤黒木の実装の検証}
+
+\chapter{まとめ}
+\section{今後の課題}
 
 %謝辞
 \addcontentsline{toc}{chapter}{謝辞}