POPL 2008メモ1日目

いつものことですが「いい加減」なメモなのでご承知＆ご容赦を…（ツッコミは歓迎します）。

今年は論文数が多いので一発表20分（質疑応答5分を含む）になったのですが、さすがにどの人もうまくまとめていて、ちょうど良いペースなのではないかと思います。もっと詳しく知りたい人はproceedingsを見る、ということで。

オープニング

  • 参加者300人以上(record high) General chairのGeorge NeculaにPC dinnerで聞いたら、POPLだけで320人らしい。VMCAI等も含めると400人ぐらいらしい。
  • Phil (Wadler)お得意の「Tシャツ暴露」。今回はSがλになっているスーパーマンTシャツ。
  • スポンサーにMozilla FoundationやDoCoMo USA Labsの名前が（ACM SIGPLAN/SIGACTと、いつものMicrosoft Research, Intel以外に）。Sunがいなくなった？

招待講演その1

  • Systems biologyの話。ちなみに話者は生化学者だが「遺伝的アルゴリズムで世界最短のpred関数（λ計算のChurch encodingで）を発見した」こともあるらしい。分子生物学的機序（パスウェイ）を、物理学的な微分方程式モデルよりも、並行計算（ペトリネットとかπ計算とか）で表現すると簡単で良いという話？　個人的には、そういうことをやっている／やっていた日本人の知り合いが多いので、さほど目新しくは感じなかった。が、プログラミング言語論の専門家が参加していて、抽象解釈などによる静的解析などもやっており、物理学的解析にきちんと対応するらしい？
    • [Q by 誰か] 自分もそういう研究をしたことがあるのだが、今後の課題は？ [A] 計算機科学者が生物学者に「解決すべき問題があったら教えて」と聞くのではなく、「こういう疑問があるのだがどうなの？」と提示するとよい？
    • PC dinnerで隣の席になって、生物と計算機科学の「文化の違い」の話に（会議論文とジャーナル論文の関係とか、査読とか）。テーブル全体で興味津々。

セッション1

定理証明によるプログラム検証のセッション。自分がsession chairだったので後で書く（時間があれば）。

  • Coqチュートリアルにも出てきた変数束縛の扱い方の話。
  • 「コンパイラの正しさ」ではなく、「コンパイル結果を検証するルーチン」の正しさを定理証明器で検証する話。例：「正しいCコンパイラ」にPowerPCの命令列スケジューリングを加えた。命令列スケジューリング自体の正当性証明が大変なので、結果を検証するルーチンの正しさを示した。
  • Parametricity（ちょっと違うらしいが）の話。多相型ソート関数の正しさは、「0と1のリスト」だけ確かめれば、任意の入力について正しいことが言える（「Knuthの0-1原理」というらしい）。同様にprefix計算アルゴリズムの正しさは「0と1と2のリスト」だけ確かめればOKという話。

セッション2

Effect systemのセッション

  • エフェクトシステム（副作用を解析する型システムのようなもの）の拡張。型つけする式の副作用だけでなく、その「前後の文脈」の副作用も型環境に含める。「e1; e2」だったら、「e2の前エフェクト」は「e1の前エフェクト」＋「e1のエフェクト」になる、といった仕組み。安全な動的アップデート（あるプログラムポイントの「前」と「後」の両方で使われているモジュールは、そこではアップデートできない？）や、マルチスレッドプログラムのメモリアクセス解析に応用。前者はvsftpdで実験。ロック解析などにも応用可能との主張。
    • [Q] 継続渡し形式にすれば？ [A] 単にCPS＋普通のエフェクトシステムだけでは駄目だが、「前後エフェクトシステム」と組み合わせれば精度は向上するかも(?)
    • [Q] Danvy-Filinskiの限定継続型システムとの関係は？ [A] その研究を知らないので調べてみる
  • STM (software transactional memory)の意味論を定式化。"strong isolation"は意味は明確だが実装が困難。"weak isolation"は実装は容易だが意味が曖昧（コードの実例あり）。意味論の定式化により、両者が等価になる（ユーザプログラムから区別できない）十分条件を定義＆証明。型・エフェクトシステムの形で。
    • [Q] 既存の実装にどれぐらい適用可能？ [A] STMはいろいろ(?)。ハードウェアはよく知らない。
  • STMの話 by Abadi。「atomicである」ほうをデフォルトにした"automatic mutual exclusion"を考えた。わざと並列にしたいときは"async"（別のtransaction）とか"unprotected"（transaction外）とか書く。weak atomicityのsemanticsは実装(optimistic concurrency)によっては非常にわかりづらいので、strong atomiciyと一致する条件(separation)を考えた（さっきの発表とは独立）。
    • [Q by Phil] STMよりmessage passing（Erlangとかjoin-calculusとか）のほうがわかりやすいのでは？ [A] STMを制限していって、つきつめればsyntaxだけの違いになるかも(!)

セッション3

Separation logic（ヒープやポインタについてのプログラム論理の一種）のセッション

  • Behavioural subtypingになっていない「悪い」inheritance（ただの"code reuse"）も扱えるプログラム検証をしたい（JMLやSPEC#では扱えない）。メソッド呼び出しの検証がdynamicで難しい（receiverの型に依存）。そこでクラスごとにabstractな述語(dynamic predicate)を定義し、それを使ってクラスのbehaviorやメソッドのspecを書く。
  • メソッドのstatic specとdynamic specをわけ、receiverのクラス（thisとかsuperとか）がわかっているときはstatic specを、わからないときはdynamic specを使う…というのはさっきの発表にもあったが、包摂されている？（独立な研究らしいが）
  • Separation logicを使ってヒープを使ったプログラムの停止性を証明したい（例：循環リストの反転）。記号的な実行がループするので、証明木も循環するが、一定の条件（サイクルの中に帰納的に定義された述語のunfoldingが含まれている）を満たせば循環した証明でも健全（帰納的に定義された述語は有限回しかunfoldできないから）かつ相対的に完全という話。

セッション4

「プログラミング言語と計算量理論」のセッション。

  • 有名なRiceの定理に「外延的等価性（の保存）」が出てくるが、そこに「計算量（の保存）」を付け加えても良いという話。「外延等価かつ計算量が同じプログラムの集まりは、trivialな場合（空集合か全体集合）のみ帰納的可算」らしい。
  • 型システムがプログラムの計算量クラスを制限するという話(implicit computational complexity)の一種。PSPACEに対応する型システムSTA_B (soft type assignment with booleans)。Cf. Soft Linear LogicはPTIME（多項式時間）に対応。
    • [Q] memoization is the trick? [A] no
  • Chris Okasaki的な関数的データ構造に、計算量をannoateして確認できるようにしたライブラリ。実装言語はAgda（≒ Haskell - 無限ループ + 依存型）。「計算量モナド」。Banker's method用にpay演算子。