|
72
|
1 \chapter{ソースコード一覧}
|
|
|
2 \label{chapter:sources}
|
|
71
|
3 本論文中に取り上げた Agda の動作するソースコードを示す。
|
|
|
4
|
|
72
|
5 \section{部分型の定義}
|
|
|
6 リスト~\ref{src:agda-subtype} に Agda 上で定義した CbC の部分型の定義を示す。
|
|
|
7
|
|
|
8 \lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda}
|
|
|
9
|
|
|
10 \section{ノーマルレベル計算の実行}
|
|
71
|
11 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
|
|
|
12 CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。
|
|
|
13
|
|
72
|
14 \lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced}
|
|
|
15
|
|
|
16 \section{メタレベル計算の実行}
|
|
|
17 \ref{section:meta-level-exec}節で取り上げたソースコードをリスト~\ref{src:meta-level-exec}に示す。
|
|
|
18
|
|
|
19 \lstinputlisting[label=src:meta-level-exec, caption=メタレベル計算例の完全なソースコード(atton-master-meta-sample.agda)] {src/atton-master-meta-sample.agda.replaced}
|
|
|
20
|
|
|
21 \section{Agda を用いた Continuation based C の検証}
|
|
|
22 \ref{section:cbc-proof}節で取り上げたソースコードを以下に示す。
|
|
|
23
|
|
|
24 \lstinputlisting[label=src:cbc-proof-cbc, caption=Agda を用いた Continuation based C の検証コード(SingleLinkedStack.cbc)] {src/SingleLinkedStack.cbc}
|
|
|
25 \lstinputlisting[label=src:cbc-proof-agda, caption=Agda を用いた Continuation based C の検証コード(stack-subtype.agda)] {src/stack-subtype.agda.replaced}
|
|
|
26
|
|
|
27 \section{スタックの実装の検証}
|
|
|
28 \ref{section:stack-proof}節で取り上げたソースコードをリスト~\ref{src:stack-proof}に示す。
|
|
|
29 \lstinputlisting[label=src:stack-proof, caption=スタックの実装の検証コード(stack-subtype-sample.agda)] {src/stack-subtype-sample.agda.replaced}
|
