No Such Blog or Diary

朝一でレジストレーションしてPADL'11で話を聞く．

初っ端の招待公演は Core i7 の formal verification の話．どうやら Pentium Pro のころから FV をやっていたらしい．仕様とか検証器とかをlazyなMLで書いてるとかいう話で，まあ手続型言語で仕様書くとか検証に関する無駄な計算を省かせるとかはしたくないから遅延評価な関数型言語でやるのは筋が良いねという．質問でロジック言語でいいんじゃねーのとか出てたけど，そこらへんは歴史的事情と現場的事情があるのでしょう．

次いで，メッセージパッシングとかネットワークの話．Erlang で，お前にはメッセージが絶対来ないよとか，お前のメッセージは絶対に受け取ってもらえないよとか，そういうメッセージのやり取りの不備を静的に解析する話．大半の発表スライドが「スライド一枚に説明したいことを連想する画像一枚」とかいう構成だったのが印象的．しゃべっていた内容は納得．パイ計算などとの関連や，セッションタイプとかとの関係があるのかないのか良くわからなかった．その次はチャネルを使ったプロセス通信なプログラムを簡単に書くコンビネータライブラリの話で，type class 使いまくると綺麗に書けるとという話．とりあえず type class を使ったプログラムは細かいことを考えなければ読みやすいのだけど，細かいことを考え出すと「この部分式の型はこれだからこのインスタンスの関数が実行されて…」とか追わなければならないので理解が大変な気がしなくもない．最後のはProbLog (Probabilistic extension of Prolog) でモバイルアドホックネットワークのプロトコルの解析を解析的にやるとか．新に解析的なのかどうかはさておき，ProbLogはプログラムに対して何かの確率をうまく計算してくれるらしい．シミュレーションとは違うのだよシミュレーションとは，と言っていたけれど，ProbLogでやってることって確率モデル（プログラム）のシミュレーションなんじゃないかなぁとか思ってみたり．まあ，よくわからん．

以下略．

オースティン到着．空港から街中までのバスが1ドルとか素晴らしすぎる．街中のバス全部が1回乗車1ドルで，一日パスでも2ドルとか．東京のバスも半額になってほしいなぁ．

さて，今日はもうレジストレーションに行ってもしょうがないので明日の朝に行くことにする．さっさと寝ないと風邪ひきそう．

だから目的地は寒くなくてもシカゴは寒いんだって！　飛行機が雪を巻き上げながら突き進んでいくし！　前回も同じようなことを思いつつ，完全に忘れてた．学習しない．

そして入国審査は例のごとく1時間かかった．こちらは学習したので乗継までの時間に余裕を持っておいた．とはいえ4時間は開けすぎだったかもしれない．

閑話休題．

PSPのUSB充電はいつでも出来るわけじゃないのね…　

明日からのお出かけの準備．まあ，いつも持ち歩いているセットに着替え付け足すだけだけど．

ああ，パスポートを忘れてはいかん．

そして飛行機で暇なので長めの論文を印刷して持っていこう．ついでに死者の宮殿の攻略情報を印刷して持ってくか．

修論生がTeXを全く使えなくて驚くばかり．過去二回の学科輪講の資料をどうやって作っていたのだろうとかいう疑問も湧いてくるのだけど…　Wordで処理してたのかね．Wordだと参照の処理とか面倒そうだし，表記法をマクロで抽象化しておいてあとで気に入らなくなったら一斉に修正とかいう技も使えなさそうだし，論文書くのにWordって使いやすいのかね？　よくわからん．科研の申請でさえ参照とか面倒だからTeXで用意してからWordに貼りつけだし．

とりあえず参照番号直打ちだけは最終的に無くさせたい所存．番号振るのはTeXのお仕事だし．"mathematical" とか入っている専攻出身でTeX使えないとかありえないし．

アンケートの集計やイベントへの参加登録等のための回答入力ページが簡単に作れつつ，入力されたデータが勝手にスプレッドシートに記録されてくれるとか便利すぎる．

でだ，大体の使い方は分かったのだけど，スプレッドシートの列の入れ替えの仕方が分からないという状況．フォームにアイテムを追加した順で列が並んでいるのだけど，フォームの上でアイテムを移動してもスプレッドシートの列が移動してくれないっぽい．別に列の順番なんか集計上は全然問題ないのだけど，何となく気持ち悪い．

もう少し Google Docs のお勉強をしなければならない様だ．