-
xhl_kogitsune
- 2057
- 0
- 1
- 0
-
- いいね！0
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
（ざっと検索した限り）どこにも書かれていないように見えるが、POPL 2014と同じ会場ホテルの隅っこのほうで、MATLABやSimulinkで有名なMathWorksの、30周年記念ワークショップ？をやっている。
2014-01-22 17:03:31
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014にて、MIT Pressの展示。日本語版TAPL持ってくれば良かった…:-) http://t.co/96J9ohU8XF
2014-01-23 06:46:18
拡大
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
そして学会の無線LANが不調になるお約束。これまで不調にならなかった例は私の知る限り日本(NII)で開催されたICFP 2011のみ。
2014-01-23 07:05:17
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
いつも私ばかり実況していて忙しいので @ksuenaga 君は公開アカウントを作って実況すること:-)＞POPL 2014
2014-01-23 07:19:12
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/Bpu3rG5yCl JavaScript言語仕様のCoq定式化（の一つ） http://t.co/mzaMKlLYxW https://t.co/ATB6CgErOI 自然言語仕様はメジャーなブラウザでも実装によって解釈が違う(!)
2014-01-23 07:36:33
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/Bpu3rG5yCl C言語の副作用完了点等の定式化。例の「(x=3)+(x=4)は未定義動作」等（cf. http://t.co/5CDtOCv0In ）
2014-01-23 07:51:40
Kohei Suenaga
@ksuenaga
POPL 2014: より表現力の高い抽象領域を使って抽象化すると悪いインバリアントが出る理由を機械学習で使われている一般化の理論で説明した話。抽象領域の VC 次元を計算してbias--variance tradeoff を調べたりする。
2014-01-23 08:12:39
Kohei Suenaga
@ksuenaga
@ksuenaga Lessons learned (1) cross validation をしよう！ (2) 抽象化は少しずつ！
2014-01-23 08:12:59
Kohei Suenaga
@ksuenaga
POPL 2014: SAT/SMT ソルバのための抽象解釈。Deduction とか abduction とかが不動点で説明できるよ！の話。
2014-01-23 08:15:29
Kohei Suenaga
@ksuenaga
@ksuenaga 全称量化と存在量化がモデルから変数を除去する操作の左随伴、右随伴（どっちがどっちかは論文を見よ）になっているそうです。へえ。
2014-01-23 08:18:15
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/Bpu3rG5yCl 前にも聞いた http://t.co/hGGboMaIJw ネットワーク設定プログラミング言語NetKatの話（話者は教員ではなく学生インターン？）。クリーネ代数に基づく等式理論等。
2014-01-23 08:20:09
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014（と併設ワークショップ等）論文無料公開中 http://t.co/PMe8BZGdKw
2014-01-23 08:30:23
Kohei Suenaga
@ksuenaga
POPL 2014: 数を数える定理（任意の数のスレッドについて P が成り立つ、の証明とか）の自動証明手法。計数オートマトンなるもので定義。このオートマトンの各状態に不変状態を付加できれば良い。
2014-01-23 08:37:10
Kohei Suenaga
@ksuenaga
@ksuenaga 基本的な戦略：できるだけ小さい計数オートマトンを学習する。プログラムのトレースを生成して、それが仕様を破らないなら、そのトレースも受理できるオートマトンを SMT ソルバに作らせる。
2014-01-23 08:39:55
Kohei Suenaga
@ksuenaga
@ksuenaga 学習したオートマトンが求める仕様の証明になっていることをペトリネットの到達可能性問題に帰着。
2014-01-23 08:41:39
Kohei Suenaga
@ksuenaga
@ksuenaga プログラムのトレースから得られる情報で証明をつくろうと試みるのは小林らの高階モデル検査の戦略に似てる感じもしますね。
2014-01-23 08:42:37
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
最近のPOPLやICFPは混んでいるコーヒーブレークでリュックを下ろす等の江戸しぐさ（）を教育すべき
2014-01-23 08:50:34
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
いつもの"PURE OCAML SINCE 2002"のTシャツ http://t.co/mBILi9YBvA
2014-01-23 08:59:56
拡大
Kohei Suenaga
@ksuenaga
並列にインバリアント生成をやらせると、アホインバリアントはすぐに出てきて、難しいインバリアントはあとで出てくる。
2014-01-23 09:25:28
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/PMe8BZGdKw こちらのアカウント:-)でも何度も言及しているCRASH/SAFEプロジェクト（セキュアCPU/OS/言語）http://t.co/PXu6xhKrhm の低レベル部分の定式化
2014-01-23 09:37:22
Kohei Suenaga
@ksuenaga
POPL 2014: 確率的プログラムのパラメタ生成。最適化問題にして解く。最急降下法が応用できるようにちょっと工夫。ノイズの影響を支配するパラメタを逐次的に求めていく。（最適化の文献でよく見る方法。）
2014-01-23 09:43:42
Kohei Suenaga
@ksuenaga
@ksuenaga 形式化はヒストグラムを抽象領域に使う。ただし、バケツが楕円になっている抽象領域。なんでか聞き逃した。
2014-01-23 09:46:52