# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485070537 -32400
# Node ID c748fb29667320fb2aad9caaf3180292a78e4ebb
# Parent  a47122d914ea027cf6249694dd1929e8fad38802
Update introduction

diff -r a47122d914ea -r c748fb296673 paper/atton-master.tex
--- a/paper/atton-master.tex	Sun Jan 22 16:24:59 2017 +0900
+++ b/paper/atton-master.tex	Sun Jan 22 16:35:37 2017 +0900
@@ -102,6 +102,7 @@
 \input{cbc.tex}
 
 \chapter{ラムダ計算と型システム}
+\label{chapter:type}
 \section{型システムとは}
 \section{型なしラムダ計算}
 \section{単純型付きラムダ計算}
@@ -109,12 +110,14 @@
 \section{部分型と Continuation based C}
 
 \chapter{証明支援系言語 Agda による証明手法}
+\label{chapter:agda}
 \section{依存型を持つ証明支援系言語 Agda}
 \section{Natural Deduction}
 \section{Curry-Howard Isomorphism}
 \section{Reasoning}
 
 \chapter{Agda における Continuation based C の表現}
+\label{chapter:subtype}
 \section{CodeSegment の定義}
 \section{DataSegment の定義}
 \section{ノーマルレベル計算の実行}
diff -r a47122d914ea -r c748fb296673 paper/cbc.tex
--- a/paper/cbc.tex	Sun Jan 22 16:24:59 2017 +0900
+++ b/paper/cbc.tex	Sun Jan 22 16:35:37 2017 +0900
@@ -1,4 +1,5 @@
 \chapter{Continuation based C}
+\label{chapter:cbc}
 
 Continuation based C (CbC)は当研究室で開発しているプログラミング言語であり、OSや組み込みソフトウェアの開発を主な対象としている。
 CbC は C言語の下位の言語であり、構文はほぼC言語と同じものを持つが、よりアセンブラに近い形でプログラムを記述する。
diff -r a47122d914ea -r c748fb296673 paper/introduction.tex
--- a/paper/introduction.tex	Sun Jan 22 16:24:59 2017 +0900
+++ b/paper/introduction.tex	Sun Jan 22 16:35:37 2017 +0900
@@ -12,7 +12,7 @@
 定理証明を行なうことができる言語には、依存型証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
 
 モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
-言語が異なれば二重で同じソフトウェアをせざるを得なくなる上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
+言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
 検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。
 そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{cbc} 言語を開発している。  %TODO: ref
 
@@ -24,8 +24,16 @@
 
 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
-また、証明的な検証として CbC における型システムを部分型として定義し、それを利用してCbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。
-
+また、証明的な検証として CbC における型システムを部分型として定義する。
+部分型を利用して CbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。
 
 
 \section{本論文の構成}
+本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
+CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算と状態を数え上げるメタ計算ライブラリ akasha の解説を行なう。
+次に第\ref{chapter:type}章で型システムについて取り上げる。
+型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。
+第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。
+Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。
+第\ref{chapter:subtype}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
+CodeSegment や DataSegment の Agda 上での定義や、メタ計算がどのように定義されるかを解説する。