--- a/paper/introduction.tex	Thu Feb 16 13:26:33 2017 +0900
+++ b/paper/introduction.tex	Thu Feb 16 13:39:49 2017 +0900
@@ -24,7 +24,7 @@
 
 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
-CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha を用いて仕様を検査する。
+CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha~\cite{atton-ipsjpro} を用いて仕様を検査する。
 また、定理証明的な検証として、 CbC のプログラムを証明支援系言語 Agda 上で証明する。
 Agda で CbC の項を表現するために部分型を用いてCbCを型付けし、Agdaでの定義からCbCの形式的な定義を得る。
 そして、Agda 上で Single Linked Stack の性質の証明を行なう。