Mercurial > hg > Papers > 2018 > nozomi-master
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 コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。