# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486877368 -32400
# Node ID 3ef3933dbd77f5bce95539c4f1cec7c6c665ac37
# Parent  ebe838b83ada59d58ab9b87f631f0f22ea8fadd9
Update

diff -r ebe838b83ada -r 3ef3933dbd77 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r ebe838b83ada -r 3ef3933dbd77 paper/summary.tex
--- a/paper/summary.tex	Sun Feb 12 11:52:20 2017 +0900
+++ b/paper/summary.tex	Sun Feb 12 14:29:28 2017 +0900
@@ -25,6 +25,7 @@
 また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。
 加えて部分型を組み込むことにより、stub の自動生成ができる。
 さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。
+他にも SingleLinkedStack の証明を元にした赤黒木の証明などが考えられる。
 
 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。