diff paper/summary.tex @ 81:3f63f697ed3a

Update
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 08 Feb 2017 17:37:08 +0900
parents 73da47f32888
children c0199291c58e
line wrap: on
line diff
--- a/paper/summary.tex	Wed Feb 08 17:25:27 2017 +0900
+++ b/paper/summary.tex	Wed Feb 08 17:37:08 2017 +0900
@@ -23,7 +23,7 @@
 その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。
 
 また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。
-加えて部分型を組み込むことにより、stub の自動生成をする。
+加えて部分型を組み込むことにより、stub の自動生成ができる。
 さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。
 
 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。