POPL 2007実況その2

朝食

  • ilogのAit Kaci氏(初対面,Jacques Garrigue氏の元ボス)やMS Researchの人たちと話.

セッション1

  • またFelleisenが自分でsession chair.招待講演を3件とも「非POPLな人」にしたことについて語っている.「モジュールやマクロの話は飽きた」?
  • Don Batory氏.ソフトウェア「工学」の人.代数や理論の知識が「普段の業務で」役に立つという話らしい.domain specificな高級言語のほうが最適化しやすい(古典的な例: SQLと関係代数)とか.継承は差分プログラミングに便利ではあるが,十分ではないのでmixinの一種が必要で,そのmixinの一種による差分プログラミングは代数的に形式化できる,とか.MakefileXML文書にも同様の構造がある(?)とか.差分プログラミングによるソフトウェアの合成をカテゴリー理論(??)で表現とか,可換図式を利用してツールを検証&デバッグとか.GenVocaとかAHEADとか出てきたが,その話は抽象的で,具体的に何をするツールなのか,ちょっとよくわからなかった….(プログラムだけじゃなくてMakefileやドキュメントも差分から合成する?)[Q] バージョン管理システムに応用できる? [A] まだやっていないが,できそう.

セッション2

  • 無線LAN不調
  • 短い休憩時間に,昨日の"Scheme & ML"の人に自分の「dynamic sealingでparametric polymorphism」について聞かれる.多相型や抽象型をサポートするために(当たり前だが)同じようなことを考えているらしい.アイディアは簡単だけど証明は大変(未解決問題)だよ,といっておく.
  • Generic programmingの実現手法であるscrap your boilerplate (SYB)をXML処理に応用した,との話.XPath, XSLT, XQueryの機能をHaskellで実装.XML文書は代数データ型の一種なので当然とも言えるかも.例によってXPathのparent pointerは守備範囲外らしい「文脈」(context)を渡すことによって親ポインタも実現できるらしい.スライドがおもしろい.("XML programming is generic programming" "What do we scrap today?" etc.)
  • 大堀先生の発表.リストだけでなく一般の再帰データ型と,foldではなく普通の再帰関数について,コンパイラが「自動で」「簡単に」適用できるfusionのアルゴリズムがほしい.実は多くのケースについて,ちょっとしたインライン展開とhoistingだけで,それができるという話.
  • 昨日の夕食でも聞いた関数プログラムの微分の話(多引数なら偏微分).発表がテイラー展開の復習から始まって笑った.Non-standard interpretationにより,実数のかわりにdual number(x0 + x1 ε + O(ε^2)の形の数)で計算をして,f(c + ε)のテイラー展開からf'(c)を逆算する.高階微分を計算するためには,実数をdual numberではなくlazyな無限数列x0 + x1 ε + x2 ε^2 + …で解釈すればよい.多変数でも基本的な考え方は同じ."functional programming has had little impact on numerical computing"といっていたが,たとえば数式処理系は関数型言語じゃないのだろうか(等と言ってみる).[Q by Phil] 微分演算子Dは参照透明なのに,参照透明な言語で実装できない,といっていたが,どういうこと? [A] 予備スライドで説明

セッション3

  • 休憩時間が(以下省略)
  • ENF bisimulationの話.自分にとっては,これが今回のメインかも(自分の研究とかぶっていて,イントロからreferされている).継続を扱っている点が貢献.というか,継続と状態の両方がないとincompleteらしい.しかし,定数(自然数や論理値)が駄目でfuture workというのはどうなのよ?(Church encodingだとx + yとy + xが等価にならない.再帰型で解決する予定らしいが.)あと,多相型や抽象型は? 自分のためのメモ:"set of relations"はSumii & Pierce (POPL 2004)以前にLassen (Dagstuhl seminar 1998, unpublished)でも提案? [Q by somebody] up-to-context? (not only evaluation context) [A] maybe not as useful as in applicative bisimulations(なんで?)[Q by me] universal/existential types? [A] not generally (maybe quantification over only first-order types such as int)
  • Standard MLなどfull scale言語の型安全性等を定理証明器で示したいという話.「ほとんどできた」らしい.言語がでかいので,自動化が必須とのこと.Definition of Standard MLの問題点も指摘("SML97 is unsound").定理証明器は(もちろん)Twelfを使ったそうだが,自分(の周囲)のPOPLmarkの経験からすると,higher-order abstract syntaxは扱いづらかった."LF/Twelf works well"とのことだが,これまで発表者&共著者と議論した経験からすると,限りなく疑わしい.実際に「logical relationを使った証明は扱えない」らしい.なお,証明が(量的に)もっとも「大変」だったのは"type specification"らしい(MLの多相型推論と型注釈の相性が微妙に悪いことは知られているはずだが).

昼食

  • (前のセッションが長引いて)食べ始めるのも遅れたが,サーブされるのも遅い!

セッション4

  • 休(略)
  • フロー解析の話.すごくad hocな気がする(←フロー解析一般にあまり興味がないので適当).
  • 「データベースとプログラミング言語の統合」系の話.ソースコードでは普通のオブジェクトみたくデータベースにアクセスできて,コンパイルすると「一個の」SQL query文字列になる(のでSQLエンジンで最適化しやすい).そのための解析は抽象解釈で実現.そういえばフランスで開催されている割には抽象解釈関係の発表が少ない? [Q by Felleisen] 関連研究たくさんあるのでちゃんと比較しろ(やや意訳)(e.g. Kleisli) [A] ?(話者が関連研究をきちんと理解していないっぽい)
  • 命令型言語のプログラムで,不変条件や減少条件(?)を推論して,ループが停止するか検証する話."Local termination analysis": プログラム全体が無限ループする場合に,「どの」ループが悪いのか,ちゃんと名指しする.Shape analysisとも組み合わせている?
  • マイクの電池切れる(2本とも).話者叫ぶが後ろの人には聞こえなさそう.会場ホテルの手抜き?
  • と思ったら,しばらくして外の音がいきなり中で流れる.:-) 外に出しておいたマイク(ワイヤレス)の電池が復活したらしい.

セッション5

  • 明日の即興5分プレゼンは希望者少(3人)でキャンセル,他のセッションを前倒し.大岩君が話そうと思っていたらしいが.
  • セキュリティのセッションらしい
  • if (input = password) then print "ok" else print "error"みたいな命令型言語のプログラムの確率的な情報漏洩(情報量の期待値や確率分布)を定量的に計算する手法.辞書攻撃に必要な長さ(?)の平均が求まったりするらしい.問題は古典的だが,ループの扱いが難しかったのを,極限で計算するとのこと.n回目までのループで漏洩する情報をWhile(cond,Body)_nとすると,lim_{n→∞} While(cond,Body)_nを計算する.それだけでも面白いが,いろいろな例がまた面白い.
  • 無線LAN不調
  • DoCoMo USA Labsの人(たち).JavaScriptをコード挿入で無害にする.日本でも同じような話を聞いたような気がするが,動的コード挿入で自己書き換えにも対応した点などが新しいらしい.セキュリティポリシーはDavid Walkerらの(security automatonではなく)edit automatonベース.ポップアップとかXSSとか,様々な「攻撃」に柔軟に対応できたとのこと.
  • プロジェクタうつらず苦労(ありがち).I/O型つきプロセスを「等価性(秘密性)を失わないで」型なしプロセスに変換する話.これにより攻撃側の型つけを仮定する必要がなくなる.昔のAbadi-Fournet-Gonthierの型つき版と思えば良い?(タイトルもオマージュっぽいし.)ちなみに,また我田引水すると,自分の「多相λ計算から暗号λ計算に変換」も同じような話なのだが,高階関数があるせいで激ムズになっている.

これから空港へ行って日本に帰るので,これでおしまい.本当にinformalな「紹介」で,(当然ながら)専門的/技術的な部分はすべて省略したので,くれぐれもご注意.