-
- いいね！0
Κeіsuke Νakanο
@ksknac
TSO は store buffer のせいで単純な interleave で捉えられない振る舞いが可能だが，CompCert を拡張して verify できるようにしたという話． #popl
2011-01-27 01:49:12
Κeіsuke Νakanο
@ksknac
C++0x の memory モデルの現行の仕様を形式化したので，検証に使ってくださいという話．ただし，その形式化の際に仕様自体に問題があることもわかったので，今の仕様は修正すべきという提案も． #popl
2011-01-27 02:28:16
Κeіsuke Νakanο
@ksknac
多重継承が可能な言語での Object のメモリレイアウトの形式化．パディングを節約した多重継承オブジェクトの複雑なレイアウトの正当性を検証できる枠組みを作ったとか．レイアウトアルゴリズムの26個の十分条件を提案． #popl
2011-01-27 02:52:56
Κeіsuke Νakanο
@ksknac
参照型を含む ML の操作的意味論でも world が再帰的に与えられるような step-indexed Kripke モデルが必要で， 超距離空間が成すカテゴリで表せるとかなんとか (適当)． #popl
2011-01-27 05:03:10
Κeіsuke Νakanο
@ksknac
高レベルと低レベルのプログラムの等価性は (低レベルでは自分自身を書き換えたりするので) 文脈等価性を考えるのが難しいが，Kripke 論理関係で表現できて GC との相性も良いとか． #popl
2011-01-27 05:25:57
Κeіsuke Νakanο
@ksknac
任意の型の値を保持できる汎用参照型のある型付きラムダを，純粋な型付きラムダに (型を変えずに) 翻訳する話．Fω を再帰的な kind と (停止する) 再帰的な型関数で拡張した「中野システム」を使う． #popl
2011-01-27 05:57:57
Κeіsuke Νakanο
@ksknac
グラフアルゴリズムを並列化するときに起こる競合のための lock を最小限にするため解析法を提案した．たとえば，Boruvka の最小全域木アルゴリズムの並列化とか． #popl
2011-01-27 07:02:11
Κeіsuke Νakanο
@ksknac
再帰的な手続きを呼び出したときの Heap や Stack の状態を抽象化する方法を提案．呼び出し状態のどの部分が frame でどの部分が footprint を推論． #popl
2011-01-27 07:34:07
Κeіsuke Νakanο
@ksknac
C++などで使われている container を index によって表現して，container の使われ方を index に対する制約として解析する．入れ子になっている container や動的な生成も正確に扱うことができる．SMT ソルバを利用．#popl
2011-01-27 07:53:01
Κeіsuke Νakanο
@ksknac
なるほど．それで隣にいた次の PC Chair が Robert Indiana の LOVE のオブジェを POPL に変えた絵を明日の発表用に一生懸命作っていたんですね．RT @esumii: POPL 2012はフィラデルフィアなのか。
2011-01-27 12:59:15
Κeіsuke Νakanο
@ksknac
DBLP の統計において POPL と最も関連が強いのは PLDI だそうだ． ESOP，ICFP，CAV，OOPSLA と続く． #popl
2011-01-27 23:59:13
Κeіsuke Νakanο
@ksknac
招待講演2，Koduの設計の話．5歳でもできるゲームプログラミング．感知，条件，動作，選択，更新 の5要素を単純化していって結局 WhenとDoの2つだけで指定するUIに． #popl
2011-01-28 00:41:28
Κeіsuke Νakanο
@ksknac
オートマトン+ストレージの空判定はストレージによって決定可能になったり決定不能になったりするが，その境界ってどこ？という話．各runに対し，ストレージへのinと対応するoutを接続してできたグラフが，MSO定義可能でbounded treewidthなら決定可能．#popl
2011-01-28 02:12:11
Κeіsuke Νakanο
@ksknac
名前のfreshnessを扱う計算モデルを表現するオートマトンの話．無限アルファベットに対する有限レジスタ付きオートマトンで，読んだ文字がレジスタのどこにあるか(又は無い=freshか)や名前の使用履歴に従って遷移する．異なる文字から成る語の集合みたいなのも受理できる．#popl
2011-01-28 02:35:56
Κeіsuke Νakanο
@ksknac
与えられたベクトルの有限集合の元を適当に選んで，有限回で目的地に辿り着くかどうか(例えば歩と桂馬の動きだけで目的のマスに進めるか) は決定可能であることが知られているが，Presburger算術によって決定できることを示した． #popl
2011-01-28 03:11:56
Κeіsuke Νakanο
@ksknac
型に基づくならし計算量解析．資源消費がどんな多項式で抑えられるかを LP ソルバで解く．たとえば，quicksort の最悪の場合 12n^2+14n+3 かかることが機械的に求まる． #popl
2011-01-28 04:58:18
Κeіsuke Νakanο
@ksknac
従来の双方向変換は get:A→B，put:A×B→Bのように非対称だったが，complement (S) を使って対称にしたものを提案．putr:A×S→B×S, putl:B×S→A×Sで，putl(a,s)=(b,s') は a,b,s' が整合するように定義．#popl
2011-01-28 05:22:57
Κeіsuke Νakanο
@ksknac
正規表現をその構造のまま型と看做すと，その型を持つ値は元の正規表現が受理したときの解析木と一致する．正規表現 R1 と R2 の包含関係は，R1 に対応する型の値から R2 に対応する型の値への変換によって証明できる．#popl
2011-01-28 05:47:52
Κeіsuke Νakanο
@ksknac
Session type に role の概念を導入．role はセッションに動的に入ったり出たりする人のコミュニケーションのパターンを記述するもので，join, leave の演算と，同じ role をもつ任意の人を表すための全称量化子を扱える枠組みを提案．#popl
2011-01-28 06:56:37
Κeіsuke Νakanο
@ksknac
「関数 f を 1 回呼んでからなら関数 g を呼ぶことが許される」というような stateful な制約を表す affine 型を導入し，OCaml 風の言語として実装した．関数の型に usage kind を追加． #popl
2011-01-28 07:27:57
Κeіsuke Νakanο
@ksknac
Rubyの型検査の話．各オブジェクトや関数の引数や返り値に型変数を割り当てて，その制約不等式を解く．if分岐で異なる型を持つような場合でも冗長なパス以外のパス毎に型を検査する．実際にライブラリの型エラーを見つけた． #popl
2011-01-28 07:59:02
Κeіsuke Νakanο
@ksknac
Most influential paper POPL 2001: Samin S. Ishtiaq, Peter W. O'Hearn: BI as an Assertion Language for Mutable Data Structures #popl
2011-01-28 08:27:26
Κeіsuke Νakanο
@ksknac
若干変な説明があったので訂正．「MSO定義可能でbounded tree-width」というのは「頭の頭痛が痛い」的でした．tree-width は空判定アルゴリズムの計算量にうまく対応するとかいうのが本質です． #popl
2011-01-28 22:56:44