-
- いいね！0
Jun Inoue
@jun0inoue
@ksuenaga 型クラスと違ってわざわざそのクラスを表す抽象型に明示的にアップキャスト?だかラップ?だかしないといけないみたいですよ。
2014-01-21 05:06:27
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
（ざっと検索した限り）どこにも書かれていないように見えるが、POPL 2014と同じ会場ホテルの隅っこのほうで、MATLABやSimulinkで有名なMathWorksの、30周年記念ワークショップ？をやっている。
2014-01-22 17:03:31
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
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
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
POPL 2014 http://t.co/PMe8BZGdKw こちらのアカウント:-)でも何度も言及しているCRASH/SAFEプロジェクト（セキュアCPU/OS/言語）http://t.co/PXu6xhKrhm の低レベル部分の定式化
2014-01-23 09:37:22
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
.@golden_lucky 座っていたMIT Pressの方が（詳しくは聞きそびれましたが）TAPL等の和訳の対応もした覚えがあるようで、http://t.co/Vtl2AxZ2Beで新刊IT書1位になった:-)と宣伝したら"Congratulations!"と言っていました！
2014-01-23 09:41:28
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
いやだから2並列セッションの（おそらく偶然？ですが）相異なる会場で:-)ちゃんと実況してるんだから公開しましょう！＞K君
2014-01-23 09:49:34
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@ksuenaga そっちの発表聞いてませんが一般に、抽象解釈で楕円は（x:=0.2x+0.4yみたいな「回転」を伴うループの変換でも保存されるので）常識みたいです
2014-01-23 09:55:49
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@ksuenaga そっちの発表聞いてませんが一般に、抽象解釈で楕円は（x:=0.2x+0.4yみたいな「回転」を伴うループの変換でも保存されるので）常識みたいです
2014-01-23 09:55:49
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
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 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
Kohei Suenaga
@ksuenaga
POPL 2014: Haskell に ML 流のシグネチャを入れようという話。Haskell はそうなってないのか。
2014-01-23 11:10:10
Kohei Suenaga
@ksuenaga
Q[オレグ氏]: 型クラスを使えばできるんじゃ？ A: 別の型クラスに言及できないのと（？）、コア言語とモジュール言語が交じるのが嫌だった。
2014-01-23 11:11:13
Kohei Suenaga
@ksuenaga
POPL 2014: 依存型プログラミング言語。停止性の証明をプログラム中に書かなくても良いのが偉い（？）停止性を強制する論理の世界と、停止性を強制しないプログラムの世界とを分けている。
2014-01-23 11:12:28