Mercurial > hg > Papers > 2018 > nozomi-master
comparison paper/sources.tex @ 72:fd984cfd5425
Add sources
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 06 Feb 2017 10:32:49 +0900 |
| parents | b0cfef1cd89f |
| children | 54cf3b3153fe |
comparison
equal
deleted
inserted
replaced
| 71:b0cfef1cd89f | 72:fd984cfd5425 |
|---|---|
| 1 \chapter{chapter:sources} | 1 \chapter{ソースコード一覧} |
| 2 \label{chapter:sources} | |
| 2 本論文中に取り上げた Agda の動作するソースコードを示す。 | 3 本論文中に取り上げた Agda の動作するソースコードを示す。 |
| 3 | 4 |
| 4 \section{ノーマルレベル動作の実行} | 5 \section{部分型の定義} |
| 5 \label{appendix:normal-level-exec} | 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{ノーマルレベル計算の実行} | |
| 6 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。 | 11 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。 |
| 7 CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。 | 12 CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。 |
| 8 | 13 |
| 9 \lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル実行の完全なソースコード] {src/atton-master-sample.agda} | 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} |