Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/introduction.tex @ 81:3f63f697ed3a

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 Wed, 08 Feb 2017 17:37:08 +0900
parents 50c2d2f1a186
children fcab76b8ca58
comparison
equal deleted inserted replaced
80:73da47f32888 81:3f63f697ed3a
28 また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。 28 また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。
29 Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。 29 Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。
30 30
31 31
32 \section{本論文の構成} 32 \section{本論文の構成}
33 % TODO: もう一回構成しなおし 33 TODO: もう一回構成しなおし
34 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。 34 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
35 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。 35 CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。
36 次に第\ref{chapter:type}章で型システムについて取り上げる。 36 次に第\ref{chapter:type}章で型システムについて取り上げる。
37 型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。 37 型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。
38 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。 38 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。