\documentclass{ipsjpapers}
\usepackage{url}
\usepackage[dvipdfmx]{graphicx}


% ユーザが定義したマクロなど．
\makeatletter
\let\@ARRAY\@array \def\@array{\def\<{\inhibitglue}\@ARRAY}
\def\<{\(\langle\)\nobreak}
\def\>{\nobreak\(\rangle\)}
\def\|{\verb|}
\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\LATEX{\iLATEX\Large}
\def\LATEx{\iLATEX\normalsize}
\def\LATex{\iLATEX\small}
\def\iLATEX#1{L\kern-.36em\raise.3ex\hbox{#1\bf A}\kern-.15em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}
\def\LATEXe{\ifx\LaTeXe\undefined \LaTeX 2e\else\LaTeXe\fi}
\def\LATExe{\ifx\LaTeXe\undefined \iLATEX\scriptsize 2e\else\LaTeXe\fi}
\def\Quote{\list{}{}\item[]}
\let\endQuote\endlist
\def\TT{\if@LaTeX@e\tt\fi}
\def\CS#1{\if@LaTeX@e\tt\expandafter\string\csname#1\endcsname\else
    $\backslash$#1\fi}

%\checklines    % 行送りを確認する時に使用
\begin{document}%{
% 和文表題
\title{hoge}
% 英文表題
\etitle{hoge}
% 所属ラベルの定義
\affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.}
% 和文著者名
\author{比嘉 健太\affiref{ie-ryukyu} \and
        河野 真治\affiref{ie-ryukyu}}
% 英文著者名
\eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and
        Shinji Kono\affiref{ie-ryukyu}}

% 和文概要
\begin{abstract}
卒業研究までの一年間で得た形式手法への感想と理想を語ろうかと．

\end{abstract}
% 英文概要
\begin{eabstract}

\end{eabstract}

% 表題などの出力
\maketitle

%}{

% 本文はここから始まる
\section{自己紹介}
私は琉球大学工学部情報工学科に所属する四年次の学生である．
自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマで取り組んでいる．

研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った．
テストを記述するコストはおそらくプログラムを書くコストと同じかそれ以上かかる．
あくまで私はプログラムのみでバグを見付けたかった．
そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することにした．

\section{卒業研究 と Category と Agda}
私の研究においてまず問題となったのがプログラムの変更の表現だった．

そこで指導教員からプログラムに対する変更を Monad によって表現するアイデアを頂いた．
アイデアを実現するために取った過程を示したい．

まず， Monad とは何かを知る必要があった．
Monad はプログラミング言語 Haskell では型クラスとして用意されており，まず型とは何かを知る必要があった．
そこで，Proofs and Types を指導教員と読むこととなった．
Proofs and Types では型と論理の対応について知ることができた．
例題は証明支援系言語 Agda によって記述した．
Agda では項とその書き換えによる等式変形を意識することとなった．

型の整合性で記述する % TODO: もうちょい書けるがまとまらない

型の理論背景を知った後，次に Monad とは一体何か知る必要があった．
Monad は Category Theory から computer science に持ち込まれたものであった．
そのために Category theory を知る必要があった．
Monad には満たすべき Monad則が存在し、Monad 則の証明も型によって Agda で記述できた。


\section{産業界に形式手法を普及するには}
\section{わたしのりそう}
\section{まとめ?}

%}

\end{document}