--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/sources.tex	Mon Feb 06 10:15:16 2017 +0900
@@ -0,0 +1,9 @@
+\chapter{chapter:sources}
+本論文中に取り上げた Agda の動作するソースコードを示す。
+
+\section{ノーマルレベル動作の実行}
+\label{appendix:normal-level-exec}
+\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}