Mercurial > hg > Papers > 2018 > nozomi-master
changeset 81:3f63f697ed3a
Update
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Feb 2017 17:37:08 +0900 |
| parents | 73da47f32888 |
| children | 39a27b704f0c |
| files | paper/abstract.tex paper/atton-master.pdf paper/cbc-type.tex paper/introduction.tex paper/summary.tex |
| diffstat | 5 files changed, 9 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/abstract.tex Wed Feb 08 17:25:27 2017 +0900 +++ b/paper/abstract.tex Wed Feb 08 17:37:08 2017 +0900 @@ -8,7 +8,7 @@ もう一つの信頼性向上手法としてデータ構造の持つ性質を証明する手法を提案する。 プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応する。 -プログラムを型付けできるよう、CbC の型システムを部分型を用いて定義する。 +CbCプログラムを型付けできるよう、CbC の型システムを部分型を用いて定義する。 加えて、型の定義を用いて証明支援系言語 Agda 上で CbC のプログラムを記述し、データ構造の性質を証明する。 \end{abstract}
--- a/paper/cbc-type.tex Wed Feb 08 17:25:27 2017 +0900 +++ b/paper/cbc-type.tex Wed Feb 08 17:37:08 2017 +0900 @@ -3,13 +3,17 @@ ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。 +CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。 +依存型を定義するためにもまず現状の CbC を型付けする必要がある。 + この章では CbC の型システムを部分型を利用して定義する。 -定義した型システムがきちんと検査されるかを確認するため、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、型付けされることを確認する。 -また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 証明する。 +定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。 +また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。 % {{{ 部分型付け \section{部分型付け} +TODO: なおす 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。 ここで、 単純型の拡張として、レコードを導入する。 @@ -511,7 +515,6 @@ \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。 -% TODO null check を入れる \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c} 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。
--- a/paper/introduction.tex Wed Feb 08 17:25:27 2017 +0900 +++ b/paper/introduction.tex Wed Feb 08 17:37:08 2017 +0900 @@ -30,7 +30,7 @@ \section{本論文の構成} -% TODO: もう一回構成しなおし +TODO: もう一回構成しなおし 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。 次に第\ref{chapter:type}章で型システムについて取り上げる。
--- a/paper/summary.tex Wed Feb 08 17:25:27 2017 +0900 +++ b/paper/summary.tex Wed Feb 08 17:37:08 2017 +0900 @@ -23,7 +23,7 @@ その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。 また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。 -加えて部分型を組み込むことにより、stub の自動生成をする。 +加えて部分型を組み込むことにより、stub の自動生成ができる。 さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。