-
xhl_kogitsune
- 2060
- 0
- 1
- 0
-
- いいね！0
Kohei Suenaga
@ksuenaga
@ksuenaga 楕円を使うのは本質的な問題ではなく、単に正確さと効率のトレードオフからのデザインチョイスらしい。
2014-01-23 09:52:26
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@ksuenaga そっちの発表聞いてませんが一般に、抽象解釈で楕円は（x:=0.2x+0.4yみたいな「回転」を伴うループの変換でも保存されるので）常識みたいです
2014-01-23 09:55:49
Kohei Suenaga
@ksuenaga
@ksuenaga Q: パラメタの敏感性の解析に金融工学で使われるが、他にどんな応用があるか。A: 機械学習。シグモイド関数でステップ関数を近似するとか。
2014-01-23 09:57:32
Kohei Suenaga
@ksuenaga
@esumii ええ、それはそうなのですが、楕円にしないと基礎の部分が何か壊れたりするのかなあと疑問に思ったところでした。
2014-01-23 09:59:16
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/Bpu3rG5yCl CakeML https://t.co/0UTIa0hzRx ML（floatやfunctorは除く）の（HOLで）形式的証明済コンパイラ（x86_64用）
2014-01-23 10:05:47
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
big-step semanticsだがlogical clockとtime outを導入して無限ループ(divergence)も扱える流行り(?)のアプローチ
2014-01-23 10:14:21
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
2並列になったおかげで1発表30分と余裕があるし、学会実況ツイートの公開は公費出張の義務の一部（わりと本気←）（まだ自分の発表が準備できていない人:-)は除く）
2014-01-23 10:17:44
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
研究者（どこの？）は型の必要性がわかっていない、という（他分野？の）研究者の発言もあったが、現実の学会は相変わらず、型の出てこない発表がない:-)
2014-01-23 10:24:30
Kohei Suenaga
@ksuenaga
POPL 2014: Functional reactive program の synthesis を無限ゲームの解を見つける問題に帰着してSMT solver+interpolation で解く。ホーン節がゲームとソルバの世界をつなぐそうな。
2014-01-23 10:28:55
Kohei Suenaga
@ksuenaga
@ksuenaga 悪い状態に行かない、良い状態にいずれ行く、その他 LTL でかける条件が仕様として使える。例としてシンデレラと継母のゲームが出てきてシンデレラがかわいそうだった。
2014-01-23 10:31:24
@simrob@mastodon.social
@simrob
So "sound compilation of the reals" is kinda like Significant Digits Go To POPL. Correct real number programming is neat. #popl2014
2014-01-23 10:39:31
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/Bpu3rG5yCl 暗号の実装コードの関係的（等価性など）かつ確率的検証。F*の拡張（ソルバはZ3）。通常のrefinement型のかわりに「L x = R x」など「左辺の値」「右辺の値」を表すL,Rつき論理式が書ける
2014-01-23 10:45:13
Kohei Suenaga
@ksuenaga
POPL 2014: 数値計算で計算結果が満たすべき仕様をプログラマに書かせて、それが成り立つことを検証。非線形計算や条件分岐にも対応。区間解析だと十分に精度が出ない。
2014-01-23 10:52:08
Kohei Suenaga
@ksuenaga
@ksuenaga 最初は区間で近似しておいて、Z3 と二分探索でできるだけ小さい区間を求めるとかしてる。条件分岐によって生じる誤差にも対応するために変数間の依存関係も見る。
2014-01-23 10:54:45
Kohei Suenaga
@ksuenaga
@ksuenaga これでプログラマが実数のレベルでコードを書いて、コンパイラが自動的に仕様を満たすギリギリの有限精度小数を選ぶとかができるようになった。
2014-01-23 10:56:02
Kohei Suenaga
@ksuenaga
Q: Why don't you use exact real? A: 効率 Q[ランジット]: ループは？ A: 今は不変条件が必要。誤差が積もるのが大変。iteration の回数で誤差を表現できないかやってる。
2014-01-23 10:59:44
Kohei Suenaga
@ksuenaga
POPL 2014: 午前のセッションの話。ミルナー賞の受賞講演。濃かった。テクニカルな内容は追い切れなかった。
2014-01-23 11:06:17
Kohei Suenaga
@ksuenaga
POPL 2014: アチーブメント賞、クゾー氏。抽象解釈のチュートリアル。型は抽象解釈だ！抽象解釈があれば型システムがなくてもその健全性が言える！（誇張）
2014-01-23 11:07:20
Kohei Suenaga
@ksuenaga
POPL 2014: 集合論的型（∧, ∨, ¬が入った型）で polymorphism がある言語。型での分岐とかできてすごい。型変数への代入を lazy に解決するのがポイントらしい。ワドラー氏が「こんなのできるってすごいなあ！でもほんとにこんなの使いたいか？」と聞いてた。
2014-01-23 11:09:29