--- a/paper/sources.tex	Mon Feb 06 10:15:16 2017 +0900
+++ b/paper/sources.tex	Mon Feb 06 10:32:49 2017 +0900
@@ -1,9 +1,29 @@
-\chapter{chapter:sources}
+\chapter{ソースコード一覧}
+\label{chapter:sources}
 本論文中に取り上げた Agda の動作するソースコードを示す。
 
-\section{ノーマルレベル動作の実行}
-\label{appendix:normal-level-exec}
+\section{部分型の定義}
+リスト~\ref{src:agda-subtype} に Agda 上で定義した CbC の部分型の定義を示す。
+
+\lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda}
+
+\section{ノーマルレベル計算の実行}
 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
 CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。
 
-\lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル実行の完全なソースコード] {src/atton-master-sample.agda}
+\lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced}
+
+\section{メタレベル計算の実行}
+\ref{section:meta-level-exec}節で取り上げたソースコードをリスト~\ref{src:meta-level-exec}に示す。
+
+\lstinputlisting[label=src:meta-level-exec, caption=メタレベル計算例の完全なソースコード(atton-master-meta-sample.agda)] {src/atton-master-meta-sample.agda.replaced}
+
+\section{Agda を用いた Continuation based C の検証}
+\ref{section:cbc-proof}節で取り上げたソースコードを以下に示す。
+
+\lstinputlisting[label=src:cbc-proof-cbc, caption=Agda を用いた Continuation based C の検証コード(SingleLinkedStack.cbc)] {src/SingleLinkedStack.cbc}
+\lstinputlisting[label=src:cbc-proof-agda, caption=Agda を用いた Continuation based C の検証コード(stack-subtype.agda)] {src/stack-subtype.agda.replaced}
+
+\section{スタックの実装の検証}
+\ref{section:stack-proof}節で取り上げたソースコードをリスト~\ref{src:stack-proof}に示す。
+\lstinputlisting[label=src:stack-proof, caption=スタックの実装の検証コード(stack-subtype-sample.agda)] {src/stack-subtype-sample.agda.replaced}