Mercurial > hg > Papers > 2018 > nozomi-master
changeset 82:39a27b704f0c
Update
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Feb 2017 17:39:12 +0900 |
| parents | 3f63f697ed3a |
| children | c0199291c58e |
| files | paper/abstract.tex paper/abstract_eng.tex paper/atton-master.pdf paper/cbc-type.tex |
| diffstat | 4 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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}
--- 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}
--- 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 で証明する。