# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486634891 -32400
# Node ID fcab76b8ca586d45567c75e5cbe3bd596c0dcacc
# Parent  2bc816f4af27fb55f55fab91be7fbffef648cdd3
Update

diff -r 2bc816f4af27 -r fcab76b8ca58 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r 2bc816f4af27 -r fcab76b8ca58 paper/atton-master.tex
--- 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 を生成するスクリプトを作ってるって書いて良い
 %    スローガンを書きたい
 %    ソースで省略しているところはそう書く
diff -r 2bc816f4af27 -r fcab76b8ca58 paper/introduction.tex
--- 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 で記述し、証明を行なう。
diff -r 2bc816f4af27 -r fcab76b8ca58 paper/master_paper.sty
--- 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{　　　　　　　　　　　　　　　　　　印}\\
       (副　査)　　　　河野　真治