--- a/paper/introduction.tex	Sun Jan 22 16:35:37 2017 +0900
+++ b/paper/introduction.tex	Mon Jan 23 10:00:41 2017 +0900
@@ -14,7 +14,7 @@
 モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
 言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
 検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。
-そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{cbc} 言語を開発している。  %TODO: ref
+そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。
 
 Continuation based C (CbC)はC言語と似た構文を持つ言語である。
 CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。
@@ -36,4 +36,4 @@
 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。
 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。
 第\ref{chapter:subtype}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
-CodeSegment や DataSegment の Agda 上での定義や、メタ計算がどのように定義されるかを解説する。
+CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。