--- a/paper/cbc-type.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/cbc-type.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -143,6 +143,27 @@
 
 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced}
 
+メタレベルの定義を部分型で行なって分かったことには以下のようなものがある。
+
+\begin{itemize}
+    \item メタ計算は階層構造化できる
+
+        メタ計算は階層構造を取ることができるため、組み合わせることも可能である。
+
+    \item 継続先が不定の場合は型を一様に扱う必要がある
+
+        メタ計算がノーマルレベルの具体的な型を知ることができるのはコンパイル時のみである。
+        よってメタ計算を定義する時は部分型制約しか記述できない。
+        逆に言えばノーマルレベル計算のみであれば部分型は解決され、レコード型で型付けができる。
+
+    \item \verb/stub/ は部分型付けにおいても必要である
+
+        GearsOS では Meta DataSegment から DataSegment を取り出すための処理として \verb/stub/ が存在していた。
+        これは Meta DataSegment で一様に扱っていた DataSegment に型を戻す処理として、型システムにおいても必要なものである。'
+        また、型システム経由で \verb/stub/ を生成することも可能であると考えられる。
+
+\end{itemize}
+
 % }}}
 
 % {{{ メタレベル計算の実行
@@ -198,7 +219,7 @@
 \section{Agda を用いた Continuation based C の証明}
 \label{section:cbc-proof}
 Agda において CbC の CodeSegment と DataSegment を定義することができた。
-実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
+実際の CbC のコードを Agda で記述し、それらの性質を証明していく。
 
 ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。
 この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。
@@ -448,7 +469,8 @@
 n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。
 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。
 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。
-なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。
-動作する完全なコードは付録に付す。
+なお、本論文で取り扱っている Agda のソースコードは可読性の向上のために暗黙的な引数を省略している。
+完全なコードは付録に付す。
 
 % }}}
+