#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
-
yoshihiro503
- 5190
- 0
- 4
- 14
-
- いいね！14
Sosuke MORIGUCHI
@chiguri
複数の高水準言語から落とせる型付き中間言語、特に並列処理用のメモリモデルを持った中間言語が欲しい。 #TPP2014
2014-12-04 16:33:34
Masahiro Sakai
@masahiro_sakai
メモリモデルを考慮した汎用型付中間言語設計に向けて (八杉 昌宏) : 型付中間言語におけるdata-race-freeが目標。面白そう。 #TPP2014
2014-12-04 16:33:59
Sosuke MORIGUCHI
@chiguri
参照やオフセット、シングルトン型は欲しい。Data-race-freeならデータについてsequential consistency。（既存の言語もそれが多い） #TPP2014
2014-12-04 16:35:47
Sosuke MORIGUCHI
@chiguri
一部の順序制約を明示することでアクセス順序の入れ替えを防ぐ。ないとハードウェアだったりコンパイラだったりが順序を変える。 #TPP2014
2014-12-04 16:37:02
Masahiro Sakai
@masahiro_sakai
raceがないことを型で保証するアプローチには例えば A Type and Effect System for Atomicity users.soe.ucsc.edu/~cormac/papers… とかあるけど、そういう方向の話? #TPP2014
2014-12-04 16:40:35
Masahiro Sakai
@masahiro_sakai
既存技術で Terauchiさんの fractional capability の話出てきた。持つ量が型の一部、持つ量に関する多相性を考えなければLPソルバで。……多相性考えるとどうなるんだろう? #TPP2014
2014-12-04 16:48:41
Masahiro Sakai
@masahiro_sakai
既存技術: concurrent separation logic 、メモリの所有権者毎に分離。 ただし、concurrent reads に未対応っぽいらしい。 確かに普通にやるとそうなりそう #TPP2014
2014-12-04 16:50:57
Masahiro Sakai
@masahiro_sakai
ロックでは厳しい並列プログラム例: データ構造の生成中はデータレースしないようにしつつ、生成後はread-onlyで利用したい。 未使用部分の情報を共有してアクセス（？）など。 #TPP2014
2014-12-04 16:53:58
Masahiro Sakai
@masahiro_sakai
@masahiro_sakai A Type and Effect System for Atomicity はロックで扱えるようなのしか扱っていない(?)から、今回の発表で問題にしているようなものは扱えない？ #TPP2014
2014-12-04 16:58:54
Masahiro Sakai
@masahiro_sakai
An intuitionistic Set-theoretical Model of the Extend Calculus of Construction (佐藤 雅大) ECCの直観主義的宇宙でのモデル?#TPP2014
2014-12-04 17:01:38
Masahiro Sakai
@masahiro_sakai
参考: ECCの元論文を昔読んだ時のメモ msakai.jp/d/?date=200605… #TPP2014
2014-12-04 17:02:25
Masahiro Sakai
@masahiro_sakai
位相空間にしたかったのは(完備)ハイティング代数になってるから、というなら最初からハイティング代数を目標にすればよいような気もするが…… #TPP2014
2014-12-04 17:18:00
Masahiro Sakai
@masahiro_sakai
Point condition 、位相空間とか locale のよく知られた条件とかに対応しないのかな？ #TPP2014
2014-12-04 17:18:39
Masahiro Sakai
@masahiro_sakai
@masahiro_sakai 項の解釈が集合の元になっているようなモデルにしたいから、とのこと。そりゃそうだ。 ただ、ハイティング代数を考えても同等にはできるはず。 参考: msakai.jp/d/?date=200812… #tpp2014
2014-12-04 17:31:09
Sosuke MORIGUCHI
@chiguri
高校だと自然数に0が入らないから、最後の問題は「解がないことを示せ」だったが、ここでは普通に入るから「解が0であることを示せ」に変わっている。 #TPP2014
2014-12-04 17:50:55