tw.log

http://twitter.com/kinaba のログ (twilog の方が便利です。)

<<newer (latest) older>>

20090122 00:34 Algorithm Design Manual は買いかどうか議論していたら次のセッションが始まっていた
20090122 00:34 [POPL] A Calculus of Atomic Actions
20090122 00:38 [POPL] こんかれんとプログラムに関するassertionとかinvariantの検証に関するアプローチ
20090122 00:39 [POPL] key idea: プログラム変換で、atomicブロックをでかくしていく
20090122 00:42 [POPL] α≦β iff s1==α==>s2 and s1==β==>s2|error
20090122 00:48 Typeのセッションまで寝そう
20090122 01:10 [POPL] Proving that non-blocking algorithms don't block
20090122 01:10 [POPL] ロックフリーの典型的な実装(CASとかで割り込まれをdetectしたらやり直し)のterminationを証明する
20090122 01:10 [POPL] terminationというのは正確にはデッドロック的状態にならないという意味(= lock-freedom)で。一個のスレッドが他から割り込まれまくって進まないという状況はまあ許す
20090122 01:10 [POPL] lock-freedomはterminationに帰着。lock-freedom⇔全部のループ内部がterminate
20090122 01:10 [POPL] 出たよせぱれーしょんろじっく。
20090122 01:10 [POPL] 例(スタック): Push/Pop/Id しかしない --> 無限にoperation繰り返したりしない --> terminateする、みたいなのをLTL+セパレーションロジックみたいなので
20090122 01:12 [POPL] 「safetyと比べてtrivialじゃね」「Concurrencyのエキスパートにとってtrivialっちゃそうなんだけどそういう直感をformalに自動的に"示せる"のがいいところ」
20090122 01:25 [POPL] A Model of Cooperative Threads
20090122 01:25 [POPL] 協調スレッドのフォーマルモデル。PCF + async C, yield, block みたいな言語
20090122 01:25 [POPL] 操作的意味論: environment に各コルーチンの実行コンテキストが入ってるようなの
20090122 01:25 [POPL] 表示的意味論: ステート(or "dode")遷移(+ "return"というマーカー)シーケンスのprefix closedなset
20090122 01:25 [POPL] returnはsequential compositionになるマーカー。asyncの中身の意味を取るところではreturnつけないで入れる
20090122 01:25 [POPL] アデカシーとフルアブストラクション成り立つ
20090122 01:25 [POPL] もっとadhocでない表示的意味論作りたい: monad on ωcpo. 不等式系でfree algebraic monadがどうとか
20090122 01:28 こーゆーのこれまでなかったということなのかな?意外だ
20090122 01:29 @wraith13 勇者にメダパニとパルプンテを食らいまくっているところ
20090122 02:10 ねっとつながんなくなった
20090122 02:54 [POPL] Static Contract Checking for Haskell
20090122 02:54 [POPL] Haskellに(Static) Contractいれてみるよー。t ::= {x| p}, {x: t1->t2}, (t1,t2), Any、でset of allowed valuesを指定できる
20090122 02:54 [POPL] head [] = BAD ; head (x:xs) = x みたいに書けたりとか。BADに行く可能性があるのはcontract違反
20090122 02:54 [POPL] inc \in x:{x|x>0} -> {y|y>1} とかみたいなpre-post-conditionの書き方
20090122 02:54 [POPL] e \in {x| p} means "e is crash-free and p(x)-/->BAD"
20090122 02:54 [POPL] crash-free は syntactic に BAD に行かないことがわかる範囲で調べる
20090122 02:54 [POPL] 実装はESC/Haskellに持ち込むだけ
20090122 02:54 [POPL] Contract自体がループしてたりCrashしたりするケースとか面白いがプレゼンするには余白がないので論文読め
20090122 02:54 [POPL] 実装的にはBADにどの関数のBADがタグつけておいてエラーメッセージ出すときに便利にしたりとか
20090122 02:56 やっぱり連投自分でもうざいなー。普通に日記の方でまとめるか。
20090122 02:57 いままでのところだと Flexible Types の話は面白かった。かなり綺麗なのでそろそろこの辺りで多相型推論の決定版としてまとまるんじゃないかなー。
20090122 03:00 質問「first class polymorphismはそんなにやたらめったら使うものではないし、そういうのを使う最重要ポイントでは、逆に型が書いてないと型のエクスパートでも読めない気がするんだけどその注釈を減らしたがってどうするの」
20090122 03:01 「定義には注釈が要る、使用側には要らない、というのが現在の落としどころで、それはそれなりにその注釈は注釈で欲しいという要求にも沿っているのではないか。ただ確かにそういう視点でもっと考える必要はあるかも」
20090122 04:28 Semantics with Applications ( http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html ) という本(の新版)が展示されてた。これプログラム意味論入門としてかなり良さそうな気がする。こんなのあったんだ
20090122 04:32 こっからパネルの前まで全く興味のわかない発表タイトルがつづいてるなあ
20090122 04:44 "Bad news: This problem is NP-complete. Good News: Can be reduced to SAT. Very efficient in practice!" そういう感覚なのか
20090122 05:07 ねむい
20090122 05:55 "Pattern Calculs" ( http://www-staff.it.uts.edu.au/~cbj/patterns/ 3月発売) て本のサンプルがあった。えらい面白そうだ。bondi という言語も面白そうだ。bondiて、おい、と思ったらシドニー人かこの人!
20090122 05:56 s/Calculs/Calculus/
20090122 05:57 全てをパターンマッチで!という。パターンマッチ厨歓喜ww
20090122 11:05 自分の実況TL読み直したら何言ってるかわからなすぎて吹いた
20090122 11:07 いや自分では記憶が残ってるからわかるんだけど、客観的に見て意味不明だ。
20090122 11:08 今日の結論はSemantics with Applications ( http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html ) 良さそうだったので誰か「ちょうど意味論勉強したいと思ってたんだ!奇遇ですね!」という人は読んでみてレビューしてください
20090122 11:14 @ranha それですそれです。て、POPL会場でdiscount priceと言ってSpringerが売りに来ている値段よりAmazon.co.jpの方が安いのはどうしたことだ…
20090122 11:15 @uskz それです。それが第何版だかわかりませんが最新版のようです。
20090122 11:20 人を煽ってばかりではなんなので僕もPattern Calculus買うか。届く頃には忘れてそうだけど…
20090122 23:00 Invited Talk "Wild Control Operators" はじまるー。自然言語とcontinuationの話っぽい。
20090122 23:02 iota作った人なのか!しらんかった
20090122 23:41 Olegさんがアップを始めたようです
20090122 23:58 SimonPJ「PLからcontinuationというのをNLに持ってて面白くなったのと逆にNLでdevelopされたアイデアでPLにもってこれそうなものはあるか」 「それは逆にこちらから聞きたいくらいだ。"the same"のところで出てきたdouble-dagger
20090122 23:59 control operator は、例外throwを、catch場所を離すのに加えて、ハンドラを実行するコンテキストをcatch場所と変えるようなconstructとしてどうだろうか」等々

<<newer (latest) older>>

presented by k.inaba (kiki .a.t. kmonos.net) under CC0