Mercurial > hg > Papers > 2017 > atton-master
changeset 101:3ef3933dbd77
Update
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Feb 2017 14:29:28 +0900 |
| parents | ebe838b83ada |
| children | 3ead244513d5 |
| files | paper/atton-master.pdf paper/summary.tex |
| diffstat | 2 files changed, 1 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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 コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。