Mercurial > hg > Papers > 2018 > nozomi-master

annotate paper/type.tex @ 28:36ce493604fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add akasha result
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 23 Jan 2017 18:41:23 +0900
parents
children 55f67e448dcc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
28
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{ラムダ計算と型システム}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 \label{chapter:type}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 \ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 CbC は直接自身を証明する機構が存在しない。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 プログラムの性質を証明するには CbC の形式的な定義が必須となる。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 \ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 \section{型システムとは}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 \section{型なしラムダ計算}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 \section{単純型付きラムダ計算}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 \section{部分型付け}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 \section{部分型と Continuation based C}