POPL 2007実況
遅いけど無線LANがある＆後で書く暇があるかわからないので実況（と思ったが，はてなが超絶不調で実況にならない…直ったようだ）．発表を聞いただけで論文は読んでいないし，どれもメモ書きレベルなので，あまり真に受け過ぎないでください．プログラムはこちら．
セッション1
- 参加者
215250人らしい（←ありがちな聞き間違い）．会場の制限で，これ以上は参加できないらしい．（この業界の）有名人多数．日本人や知り合い多し．あと，MS関係者も（必ずしもMS Researchに限らず）． - Tang氏の招待講演はドタキャン(!)．"Family emergency"らしい．
- しょうがないので3日目の招待講演を急遽移動．IBMのChet Murthy氏．オンラインバンキングシステム（大手，複数）の内部XML処理コンポーネントへの，プログラミング言語理論（ML，type specialization，deforestation等々）の適用事例について．当たり前かもしれないが，お客さんには言語や理論は隠して，「今までのシステムより軽い」とか，ビジネス上のメリットを言っておけ，とのこと．
- Murthy氏の招待講演を前倒ししたので，3日目の朝は即興5分発表のセッションにするらしい．が，自分は2日目の夕方出発…
セッション2
- DrSchemeのグループからの発表．話者はRobby FindlerではなくJacob Matthews氏．.NET等でSchemeとMLを混ぜて使う話．特に目新しい点が見当たらないのだが，どういう貢献が評価されたのだろうか．[Q by Phil Wadler] 型安全性はどうなるの？ [A] If something goes wrong, it's Scheme's fault. (laughter)
- AOPの話．AspectJのpointcutの意味論を論理型言語(Datalog)への変換で定義するらしい．アスペクト指向自体が？？？なので，これも何がうれしいのかピンと来ない．AOPのsemanticsとして，Wandの論文はreferされているが，増原さんの論文がreferされていない（直接の関係はないのかもしれないが）．
- 型付き低水準言語系の話．多重継承の実装方法．interior pointer（メモリ領域の途中へのポインタ）の型つけのしかたが新しい？
セッション3
- 休憩時間，短し．会場もプログラムも過密？
- 無線LAN，ユーザ過多で不調（ありがち）．っていうかつながらない．「つなぎっぱなしにしないで」とアナウンス．
- POPLでは少数派？（PLDIでは多数派？）の実行時解析系のセッション．
- 「GCを応用してメモリリークを検出」系の話．JVMに実装．Eclipseなどのメモリリークを検出，原因を特定して修正．
- Conservative GCやphysical subtypingのアイディアを使って，C言語でヒープの中身を「実行時型検査」する話．
- 今回のPOPL，少し女性話者多い？
- 動的テスト生成の話．「動的だから静的な手法より強力」というnaiveな主張だが，例が嘘っぽい（最近のソフトウェアモデル検査の手法を応用すれば静的にテストできそう）．「動的」「静的」の定義の問題かもしれないが，じゃあソフトウェアモデル検査との差分は？？？ テストの「生成」が目的としても，生成されたテストはいずれ実行されるし．質疑応答で同じ質問，同じ説明（になっていないが）．
- キャッシュの話（←おおざっぱ過ぎ）
昼食
- Andy Gordonと，Wadlerのところの学生さんの間に座る（その隣は稲葉くん，さらに隣はOege de Moor）．Linksの話など．
- 10年前（POPL 1997）の"most influential paper" awardの贈呈．Neculaのproof carrying codeの論文が受賞．まあ当然だろう．
セッション4
- だから休憩時間が短いってば！ 食べ終わったばかりで，コーヒーを飲（んで他の人と話し込）む暇もない．
- このブログでも前に出てきた，MLのモジュールシステム＋αで，Haskellの(associated) type class＋α'も表す，という話．Wadlerの質問時間切れ，session chairのPatrick Cousotが強制終了（笑）．
- 自由変数（定数）に，通常と異なる値を割り当てて式を評価する"non-standard interpretation"の実現方法に関する話．クロージャの中の自由変数の値を書き換えるmap-closureという構文を提案，通常のクロージャ変換を拡張して実装（Cf. call/ccとCPS変換）．[Q by Felleisen] クロージャの表現が固定されてしまうのでは？ [A] map-closureの実装で複数の表現を処理すればOK
- PADS/ML．httpdのログとか，いろいろなテキスト（ないしバイナリ）フォーマットにMLみたいなデータ型を与えて，高速に処理したり，parserやprinterを自動生成したり，という話（は前からあるが，その一つ）．
- FreshMLの話（の一つ）．メタプログラミング（プログラムを処理するプログラムの開発）のために，変数の束縛とかα変換とか名前生成とかの機能を内蔵したML．λx.eとかあったら，unbind(λx.e)とかすると，freshなx'に対して(x', [x'/x]e)とかが得られる．そのx'に対していろいろな操作や観察ができるけど，「α同値な項はメタ文脈等価である」という性質は失われない，という意外な結果．第二著者がGCCをメンテしてる会社に就職したらしい．[Q by Simon Peyton Jones] future workで「対象プログラムのα同値性だけでなく文脈等価性を考慮したい」といったが，ほとんどのメタ観察は文脈等価なプログラムを区別するのでは？ [A] 観察による(?)
セッション5
- Separation logic系の話．エイリアスしうるポインタとかヒープメモリとかについての性質を検証するためのプログラム論理．OSみたいなシステムレベルのCコードの正しさを検証したい．とりあえずkmallocの正しさを定理証明器上で検証したらしい．ちょっと「力ずく」っぽいが，メモリ上のデータを（抽象化しすぎないで）ちゃんとバイトレベルで定式化したとのこと．正確にはバイトレベルの表現と値レベルの表現を定義して，必要に応じて両方を行き来できるようにした．
- Foundational proof carrying code系の話（実行系まで安全性の証明が付加されたプログラミング言語システムを構築したい）．証明を簡単にするために，意味論的型つけ(semantic typing)を用いたい．そのためには，非叙述的多相型と（破壊的代入の可能な）参照セルを両方ともサポートするsemanticsが必要．Appel/Ahmedらのindexed modelと，中野のmodal modelを利用して，そういうKripke semanticsを構築したとのこと(cf. [Nakano 2000])．自分の研究に我田引水すると，安全性（一項関係）だけでなく等価性（二項関係）の証明にも有用かどうか？ [Q by somebody] Scottの不動点帰納法との関係は? [A] わからないが，domain theoryのかわりに自然数ベースの初等的モデル(indexed model)を利用している(?)
- Separation logicやambient logic（＆その拡張であるcontext logic）を様相論理の一種で解釈する，という話？
"Business meeting"
General chair report (Martin Hofmann)
- いつもの「運営側関係者に感謝して拍手」
- 予算$90,000（うちMSから$3,600寄付）
- レセプションは明日7:30pmから（参加できないけど…）
Program chair report (Felleisen)
- いつもの分野／地域の分布…は省略！（面倒くさいから？）
- プログラム委員／招待講演／論文のselectionについて
- "Chet Murthy: modern PL research have an impact on multi-million dollar products"
- "Don Batory: software engineering research constantly intersects with PL research"
- "Audrey Tang: an autodidact who took Benjamin Piece (too) seriously; her work on Perl 6"（FelleisenはLL1で初めて会った？）
- short paperについて：91% authors willing, 13 selected
- two rounds voting with "paper dollar" system (program chair had no votes)
- 来年のプログラム委員長はWadler，場所はサンフランシスコで検討中
夕食
