Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/introduction.tex @ 95:fcab76b8ca58

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 19:08:11 +0900
parents 3f63f697ed3a
children ebe838b83ada
comparison
equal deleted inserted replaced
94:2bc816f4af27 95:fcab76b8ca58
28 また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。 28 また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。
29 Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。 29 Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。
30 30
31 31
32 \section{本論文の構成} 32 \section{本論文の構成}
33 TODO: もう一回構成しなおし
34 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。 33 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
35 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。 34 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、GearsOS の解説を行なう。
35 第\ref{chapter:akasha}章にて GearsOS 上の非破壊赤黒木の検証をメタ計算ライブラリ akasha にて行なう。
36 次に第\ref{chapter:type}章で型システムについて取り上げる。 36 次に第\ref{chapter:type}章で型システムについて取り上げる。
37 型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。 37 型システムの定義と CbC の型システムの定義に必要な単純型、レコード型、部分型について述べる。
38 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。 38 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。
39 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。 39 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。
40 第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。 40 第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
41 CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。 41 CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。