\section{Agda}
Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
は記述したプログラムを証明することができる。

%\subsection{Record 型}

%\subsection{Data 型}

%\subsection{Agdaの基本操作}

%\subsection{定理証明支援器としての Agda}

%\subsectoin{}