--- a/paper/summary.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/summary.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -8,7 +8,7 @@
 
 二つめは定理証明的なアプローチである。
 akasha を用いた検証では挿入回数は有限の数に限定されていた。
-データ構造とそれにまつわる処理を直接証明することにより、任意の回数操作を行なっても性質を保証する。
+プログラムを直接証明することにより、任意の回数の操作においても性質を保証する。
 部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。
 Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。
 
@@ -30,4 +30,4 @@
 
 また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。
 多相型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
-他にも、CbC における型推論や推論器のコンパイラへの実装などが挙げられる。
+他にも、CbC の型推論や推論器の実装などが挙げられる。