# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486704343 -32400
# Node ID 0a4646310261482849d46daf0f8fbeb7aa0f5949
# Parent  fcab76b8ca586d45567c75e5cbe3bd596c0dcacc
Update

diff -r fcab76b8ca58 -r 0a4646310261 paper/abstract.tex
--- a/paper/abstract.tex	Thu Feb 09 19:08:11 2017 +0900
+++ b/paper/abstract.tex	Fri Feb 10 14:25:43 2017 +0900
@@ -6,9 +6,9 @@
 一つはプログラムが持つ状態を数え挙げ、常に仕様を満たすことを保証するモデル検査的手法である。
 プログラムの実行を網羅的に行なうよう変更するメタ計算ライブラリ akasha を用いて赤黒木の仕様を検証する。
 
-もう一つの信頼性向上手法としてデータ構造の持つ性質を証明する手法を提案する。
-プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応する。
-CbCプログラムを型付けできるよう、CbC の型システムを部分型を用いて定義する。
-加えて、型の定義を用いて証明支援系言語 Agda 上で CbC のプログラムを記述しデータ構造の性質を証明する。
+もう一つの信頼性向上手法として、プログラムのデータ構造の性質を証明する手法を提案する。
+プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応している。
+CbC プログラムの性質を証明できるよう、部分型を用いてCbC の型システムを定義する。
+加えて、型システムの定義を用いて証明支援系言語 Agda 上に CbC のプログラムを記述し、証明を行なう。
 
 \end{abstract}
diff -r fcab76b8ca58 -r 0a4646310261 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed