Mercurial > hg > Papers > 2017 > atton-master
changeset 95:fcab76b8ca58
Update
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 09 Feb 2017 19:08:11 +0900 |
parents | 2bc816f4af27 |
children | 0a4646310261 |
files | paper/atton-master.pdf paper/atton-master.tex paper/introduction.tex paper/master_paper.sty |
diffstat | 4 files changed, 10 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/atton-master.tex Thu Feb 09 18:58:53 2017 +0900 +++ b/paper/atton-master.tex Thu Feb 09 19:08:11 2017 +0900 @@ -1,16 +1,11 @@ % TODO lists % 比較対象 % agda の stack? -% akasha は別 chapter にして -% あと増量させる % あと syntax を最新に合わせて動かしてくれ % type system に名前を付ける? % 先の展望を書くべきだな % delta monad % csComp, push-pop, exec-comp の解説 -% 型システムの説明は付録に -% というか説明が良くない -% ポンチ絵を増やして良い(meta とかの上書き) % stub を生成するスクリプトを作ってるって書いて良い % スローガンを書きたい % ソースで省略しているところはそう書く
--- a/paper/introduction.tex Thu Feb 09 18:58:53 2017 +0900 +++ b/paper/introduction.tex Thu Feb 09 19:08:11 2017 +0900 @@ -30,11 +30,11 @@ \section{本論文の構成} -TODO: もう一回構成しなおし 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。 -CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。 +CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、GearsOS の解説を行なう。 +第\ref{chapter:akasha}章にて GearsOS 上の非破壊赤黒木の検証をメタ計算ライブラリ akasha にて行なう。 次に第\ref{chapter:type}章で型システムについて取り上げる。 -型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。 +型システムの定義と CbC の型システムの定義に必要な単純型、レコード型、部分型について述べる。 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。 第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
--- a/paper/master_paper.sty Thu Feb 09 18:58:53 2017 +0900 +++ b/paper/master_paper.sty Thu Feb 09 19:08:11 2017 +0900 @@ -18,7 +18,7 @@ % % %\jtitle{修士論文スタイルファイル\\自律分散研バージョン} -%\etitle{\LaTeX style test file for master paper} +%\etitle{\LaTeX style test file for master paper} %\year{平成11年度} %\affiliation{琉球大学大学院理工学研究科\\ 情報工学専攻} %\author{名字 名前} @@ -147,18 +147,18 @@ \newpage\null \thispagestyle{empty} \vskip 1cm% - + \begin{center}% \let\footnote\thanks {\Large\bf\thesis\\} {\Large\bf\ethesis\vskip 0.4em} - + {\LARGE\bf\mc\@title\\} {\LARGE\bf{\@etitle}\vskip 0.4 em} {\large\mc\@year\\} {\large\@eyear\vskip 0.3 em} - + {\large\bf\mc\@author\par} {\large\bf\@eauthor\par\vskip 0.8 em} @@ -171,7 +171,7 @@ {\large\textbf\ecourse\\} {\large\textbf\edepartment\\} {\large\textbf\euniversity\vskip 0.3em} - + {\large\bf\mc\@chife\\} {\large\bf\@echife\\} \end{center} @@ -197,10 +197,10 @@ (主 査) 和田 知久 \vskip 2 em \underline{ 印}\\ - (副 査) 岡﨑 威生 + (副 査) 岡崎 威生 \vskip 2 em \underline{ 印}\\ - (副 査) 名嘉村 盛和 + (副 査) 名嘉村 盛和 \vskip 2 em \underline{ 印}\\ (副 査) 河野 真治