# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1487219989 -32400
# Node ID 18f872806bc09dd7d959885c74bbc1342def24b4
# Parent  c1cc5407cefee29d68d24180e495319136b6855a
Update reference

diff -r c1cc5407cefe -r 18f872806bc0 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r c1cc5407cefe -r 18f872806bc0 paper/introduction.tex
--- 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 の性質の証明を行なう。
diff -r c1cc5407cefe -r 18f872806bc0 paper/reference.bib
--- a/paper/reference.bib	Thu Feb 16 13:26:33 2017 +0900
+++ b/paper/reference.bib	Thu Feb 16 13:39:49 2017 +0900
@@ -166,6 +166,11 @@
     year   = "2016"
 }
 
+@misc{atton-ipsjpro,
+    author = "比嘉 健太, 河野 真治",
+    title  = "Continuation based C を用いたプログラムの検証手法",
+}
+
 @book{Pierce:2002:TPL:509043,
     author = {Pierce, Benjamin C.},
     title = {Types and Programming Languages},