--- a/paper/cbc-type.tex	Wed Feb 01 15:27:15 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 01 15:37:11 2017 +0900
@@ -55,7 +55,33 @@
 正しく計算が行なえたなら値150が得られるはずである。
 % }}}
 
+% {{{ ノーマルレベル計算の実行
 \section{ノーマルレベル計算の実行}
+プログラムを実行することは \verb/goto/ を定義することと同義である。
+軽量継続\verb/goto/ の性質としては
+
+\begin{itemize}
+    \item 次に実行する CodeSegment を指定する
+    \item CodeSegment に渡すべき DataSegment を指定する
+    \item 現在実行している CodeSegment から制御を指定されて CodeSegment へと移動させる
+\end{itemize}
+
+がある。
+Agda における CodeSegment の本体は関数である。
+関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。
+よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。
+
+この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。
+具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。
+
+\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}
+
+この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。
+本文中での CodeSegment の定義は一部を抜粋している。
+実行可能な Agda のソースコードは付録に載せる。% TODO: Appendix
+
+% }}}
+
 \section{MetaDataSegment の定義}
 \section{MetaCodeSegment の定義}
 \section{メタレベル計算の実行}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/Goto.agda	Wed Feb 01 15:37:11 2017 +0900
@@ -0,0 +1,4 @@
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+   -> CodeSegment I O -> I -> O
+goto (cs b) i = b i
+