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