% withpage: ページ番号をつける (著者確認用)
  % english: 英語原稿用フォーマット
  \documentclass{ipsjprosym}
  %\documentclass[withpage,english]{ipsjprosym}
  \usepackage{listings}
  \usepackage[dvipdfmx]{graphicx}
  \usepackage{latexsym}
  \usepackage{comment}
  \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}}

\begin{document}

% Title, Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{GearsOS の Agda による記述と検証}

\affiliate{IPSJ}{情報処理学会}

\author{外間 政尊}{Masastaka HOKAMA}{}[masataka@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{IPSJ}[kono@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{jkeyword}
OS, プログラミング言語, CbC, Gears OS, Agda
\end{jkeyword}

\maketitle

% Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{}

% BibTeX を使用する場合 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{ipsjsort}
\bibliography{prosym}

% BibTeX を使用しない場合
%\begin{thebibliography}{9}
%\bibitem{latex}玉城将士、谷成雄，河野真治 : \textbf{Cassandraを使ったスケーラビリティのあるCMSの設計 }. 情報処理学会システムソフトウェアとオペレーティング・システム研究会、 2011.
%\bibitem{latex}玉城将士 : \textbf{非破壊的木構造を用いた分散CMSの設計と実装 }. 琉球大学理工学研究科修士論文、2013
%\bibitem{latex}大城信康 、杉本優 、河野真治 : \textbf{Data Segment の分散データベースへの応用}. 日本ソフトウェア科学会第30回大会論文集. 、2013
%\bibitem{latex}大城信康 : \textbf{分散Database Jungleに関する研究}. 琉球大学理工学研究科修士論文、2014
%\bibitem{latex}金川竜己、河野真治 : \textbf{非破壊的木構造データベースJungleとその評価  }. 情報処理学会システムソフトウェアとオペレーティング・システム研究会、 2015.
%\end{thebibliography}
\end{document}