Mercurial > hg > Papers > 2017 > atton-master

changeset 126:18f872806bc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update reference
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 16 Feb 2017 13:39:49 +0900
parents c1cc5407cefe
children 7903c02fe686
files paper/atton-master.pdf paper/introduction.tex paper/reference.bib
diffstat 3 files changed, 6 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
Binary file paper/atton-master.pdf has changed
--- 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 の性質の証明を行なう。
--- 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},