--- a/paper/chapter/02-cbc.tex	Tue Feb 02 14:17:05 2021 +0900
+++ b/paper/chapter/02-cbc.tex	Tue Feb 02 14:41:18 2021 +0900
@@ -5,7 +5,7 @@
 またCbCではこの軽量継続を用いて\texttt{for}文などのループの代わりに再起呼び出しを行う。
 これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。
 Agda よる関数型のCbCの記述も用意されている。
-実際のOSやアプリケーションを記述する場合には、GCC及びLLVM/clang上のCbC実装を用いる。
+実際のOSやアプリケーションを記述する場合には、GCC\cite{cbcgcc}及びLLVM/clang上\cite{cbcllvm}のCbC実装を用いる。
 
 
 \section{CodeGear}
@@ -47,8 +47,6 @@
 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
-CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears}
-現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。
 
 \section{メタ計算}
 プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。