changeset 96:0a4646310261 1F-submit

Update
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 10 Feb 2017 14:25:43 +0900
parents fcab76b8ca58
children 5a354cba3694
files paper/abstract.tex paper/atton-master.pdf
diffstat 2 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- 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}
Binary file paper/atton-master.pdf has changed