changeset 73:a92ac75bd9fa

Add abstract
author atton <>
date Mon, 06 Feb 2017 15:42:45 +0900
parents fd984cfd5425
children e9ff08a232f7
files paper/abstract.tex paper/abstract_eng.tex paper/atton-master.pdf
diffstat 3 files changed, 22 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/paper/abstract.tex	Mon Feb 06 10:32:49 2017 +0900
+++ b/paper/abstract.tex	Mon Feb 06 15:42:45 2017 +0900
@@ -1,3 +1,14 @@
+本論文では Continuation based C(CbC) 言語で記述されたプログラムを検証用に変更せず信頼性を確保する手法を二つ提案する。
+プログラムの実行を網羅的に行なうよう変更するメタ計算ライブラリ akasha を用いて赤黒木の仕様を検証する。
+プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応する。
+プログラムを型付けできるよう、CbC の型システムを部分型を用いて定義する。
+加えて、型の定義を用いて証明支援系言語 Agda 上で CbC のプログラムを記述し、データ構造の性質を証明する。
--- a/paper/abstract_eng.tex	Mon Feb 06 10:32:49 2017 +0900
+++ b/paper/abstract_eng.tex	Mon Feb 06 15:42:45 2017 +0900
@@ -1,3 +1,13 @@
+Checking desirable specifications of software are important.
+If it checks actual implementations, much better.
+In this papaer, We propose two verification methods using meta computations which save original implementations.
+On the hand method verify specification by enumerate possible states on programs.
+We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively.
+On the other hand method veriy programs with proofs.
+Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
+We define the CbC type system with subtype for proving CbC itself.
+Agda proves properties of translated CbC programs using proposed subtype definition.
Binary file paper/atton-master.pdf has changed