# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486543152 -32400
# Node ID 39a27b704f0c67eb4a5bd03c19f929553210be75
# Parent  3f63f697ed3a6237df05d48281caf5d3f33006cc
Update

diff -r 3f63f697ed3a -r 39a27b704f0c paper/abstract.tex
--- a/paper/abstract.tex	Wed Feb 08 17:37:08 2017 +0900
+++ b/paper/abstract.tex	Wed Feb 08 17:39:12 2017 +0900
@@ -9,6 +9,6 @@
 もう一つの信頼性向上手法としてデータ構造の持つ性質を証明する手法を提案する。
 プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応する。
 CbCプログラムを型付けできるよう、CbC の型システムを部分型を用いて定義する。
-加えて、型の定義を用いて証明支援系言語 Agda 上で CbC のプログラムを記述し、データ構造の性質を証明する。
+加えて、型の定義を用いて証明支援系言語 Agda 上で CbC のプログラムを記述しデータ構造の性質を証明する。
 
 \end{abstract}
diff -r 3f63f697ed3a -r 39a27b704f0c paper/abstract_eng.tex
--- a/paper/abstract_eng.tex	Wed Feb 08 17:37:08 2017 +0900
+++ b/paper/abstract_eng.tex	Wed Feb 08 17:39:12 2017 +0900
@@ -9,5 +9,5 @@
 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.
+Dependent-typed language Agda proves properties of translated CbC programs using proposed subtype definition.
 \end{abstract_eng}
diff -r 3f63f697ed3a -r 39a27b704f0c paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r 3f63f697ed3a -r 39a27b704f0c paper/cbc-type.tex
--- a/paper/cbc-type.tex	Wed Feb 08 17:37:08 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 08 17:39:12 2017 +0900
@@ -4,9 +4,9 @@
 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
 
 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
-依存型を定義するためにもまず現状の CbC を型付けする必要がある。
+依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。
 
-この章では CbC の型システムを部分型を利用して定義する。
+~\ref{chapter:cbc-type}では CbC の型システムを部分型を利用して定義する。
 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。