--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/sigos.tex	Fri Apr 13 18:07:04 2018 +0900
@@ -0,0 +1,97 @@
+\documentclass[techrep]{ipsjpapers}
+\usepackage[dvipdfmx]{graphicx}
+\usepackage{url}
+\usepackage{listings,jlisting}
+\usepackage{enumitem}
+
+\lstset{
+    language=C, 
+    tabsize=2, 
+    frame=single, 
+    basicstyle={\ttfamily\footnotesize},% 
+    identifierstyle={\footnotesize},% 
+    commentstyle={\footnotesize\itshape},% 
+    keywordstyle={\footnotesize\bfseries},% 
+    ndkeywordstyle={\footnotesize},% 
+    stringstyle={\footnotesize\ttfamily}, 
+    breaklines=true, 
+    captionpos=b, 
+    columns=[l]{fullflexible},% 
+    xrightmargin=0zw,% 
+    xleftmargin=1zw,% 
+    aboveskip=1zw, 
+    numberstyle={\scriptsize},% 
+    stepnumber=1, 
+    numbersep=0.5zw,% 
+    lineskip=-0.5ex, 
+}
+\renewcommand{\lstlistingname}{Code}
+\usepackage{caption}
+\captionsetup[lstlisting]{font={small,tt}}
+
+\input{dummy.tex} %% Font 
+
+% ユーザが定義したマクロなど．
+\makeatletter
+
+\begin{document}
+
+% 和文表題
+\title{GearsOS の Agda による記述と検証}
+% 英文表題
+\etitle{}
+
+% 所属ラベルの定義
+\affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
+\affilabel{2}{琉球大学工学部情報工学科\\Information Engineering, University of the Ryukyus.}
+
+% 和文著者名
+\author{
+  外間 政尊\affiref{1}
+  \and
+  河野 真治\affiref{2}
+}
+
+% 英文著者名
+\eauthor{
+  Masataka HOKAMA\affiref{1}
+  \and
+  Shinji KONO\affiref{2}
+}
+
+% 連絡先（投稿時に必要．製版用では無視される．）
+\contact{外間 政尊\\
+        〒903-0213 沖縄県西原町千原1番地\\
+	琉球大学工学部情報工学科\\
+        TEL: (098)895-2221\qquad FAX: (098)895-8727\\
+        email: masataka@cr.ie.u-ryukyu.ac.jp}
+
+% 和文概要
+\begin{abstract}
+    Gears OS は継続を主とするプログラミング言語 CbC で記述されている。 OS やアプリケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。 確認方法にはモデル検査と証明がある。 ここでは定理証明支援系Agdaを用いた、CbC 言語の証明方法を考える。 CbC は関数呼び出しを用いず goto 文により遷移する。 これを継続を用いた関数型プログラムとして記述することができる。 この記述はAgda上で決まった形を持つ関数として表すことができる。 Gears OS のモジュールシステムは、実装とAPI を分離することを可能にしている。 このモジュールシステムを Agda 上で記述することができた。 継続は不定の型を返す関数で表されるので、継続に直接要求仕様を Agda の論理式として渡すことができる。 継続には仕様以外にも関数を呼び出すときの前提条件(pre-condition)を追加することが可能である。 これにより、Hoare Logic 的な証明を Agda で記述した CbC に直接載せることが可能になる。 Agda で記述された CbC と実装に用いる CbC は並行した形で存在する。 つまり、CbC のモジュールシステムで記述されたプログラムを比較的機械的に Agda で記述された CbC 変換することができる。 本論文ではAgda 上での CbC の記述手法とその上での Hoare Logic 的な証明手法について考察する。
+\end{abstract}
+
+% 英文概要
+\begin{eabstract}
+\end{eabstract}
+
+% 表題などの出力
+\maketitle
+
+% 本文はここから始まる
+
+% Introduce
+% Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
+
+% 研究目的
+
+% 信頼性の高いOS
+
+\section{OS での信頼性の保証}
+test
+
+\nocite{*}
+\bibliographystyle{ipsjunsrt}
+\bibliography{sigos}
+
+\end{document}