--- a/paper/abstract.tex	Sun Feb 12 10:45:45 2017 +0900
+++ b/paper/abstract.tex	Sun Feb 12 11:13:08 2017 +0900
@@ -7,11 +7,11 @@
 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ Akasha として実装した。
 Akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
 
-木の大きさを制限せず実装が仕様を満たしていることを示すには証明が必要である。
+木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。
 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
 本論文では依存型を持つ証明支援系 Agda を用いて証明を行なう。
 部分型を用いてCbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。
-これらの形式的定義を Agda によって記述し、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質を証明した。
+これらの形式的定義を Agda によって記述し、Single Linked Stackの満たす性質を証明した。
 
 \end{abstract}
 
@@ -28,6 +28,6 @@
 Proofs in a program are known to correspond $\lambda$ calculus, which is a Curry-Howward Isomorphism.
 We use dependently typed Agda proof assistance system.
 Formal definitions of CbC are similarly defined by subtyped CbC terms using Agda.
-We prove associativity of CbC code and Properties of Single Linked Stack using proposed formal definitions.
+We prove properties of Single Linked Stack using proposed formal definitions.
 \end{abstract_eng}
 

Binary file paper/atton-master.pdf has changed

--- a/paper/cbc-type.tex	Sun Feb 12 10:45:45 2017 +0900
+++ b/paper/cbc-type.tex	Sun Feb 12 11:13:08 2017 +0900
@@ -193,9 +193,9 @@
 
 % }}}
 
-% {{{ Agda を用いた Continuation based C の検証
+% {{{ Agda を用いた Continuation based C の証明
 
-\section{Agda を用いた Continuation based C の検証}
+\section{Agda を用いた Continuation based C の証明}
 \label{section:cbc-proof}
 Agda において CbC の CodeSegment と DataSegment を定義することができた。
 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
@@ -270,8 +270,8 @@
 
 % }}}
 
-% {{{ スタックの実装の検証
-\section{スタックの実装の検証}
+% {{{ スタックの実装の証明
+\section{スタックの実装の証明}
 \label{section:stack-proof}
 定義した SingleLinkedStack に対して証明を行なっていく。
 ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。
@@ -364,7 +364,8 @@
 全く値を変更しない CodeSegment \verb/id/ を指定した際には自明にこの性質が導ける。
 実際、 Agda 上でも等式変形を明示的に指定せず、定義からの推論でこの証明を導ける(リスト~\ref{src:agda-push-pop-proof})。
 
-なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリ(\verb/Data.Nat/)における自然数型 $ \mathbb{N} $ としている。
+なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリの(\verb/Data.Nat/)モジュールにおける自然数型 $ \mathbb{N} $ としている。
+これはスタックを利用する際に具体的な値があると証明に有用であるからである。
 push/pop 操作の後の継続が \verb/Meta/ に影響を与えない制約は \verb/id-meta/ に表れている。
 これは \verb/Meta/ を構成する要素を受け取り、継続先の CodeSegment に恒等関数 \verb/id/ を指定している。
 加えて、スタックが空で無い制約 where 句の \verb/meta/ に表れている。
@@ -399,7 +400,8 @@
 
 \begin{itemize}
     \item 「n回pushした後にn回popしても同様になる」という定理を \verb/n-push-pop/ とおく。
-    \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである
+    \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \\
+        \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである
     \item 特定の \verb/Meta/ とは、 push/pop 操作の後の継続が DataSegment を変更しない \verb/Meta/ である。
     \item また、簡略化のために \verb/csComp/ による CodeSegment の合成を二項演算子 \verb/./ とおく
         \begin{itemize}