# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484551722 -32400
# Node ID f6931d3d59c07eb3bc379afe36040c5b4f41a9a7
# Parent  debfed0aa2e4eb956667ae981654944e81a01ce8
Add first table of contents

diff -r debfed0aa2e4 -r f6931d3d59c0 paper/atton-master.tex
--- 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}{謝辞}