\chapter{ソースコード一覧}
\label{chapter:sources}
本論文中に取り上げた Agda の動作するソースコードを示す。

\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=ノーマルレベル計算例の完全なソースコード(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}