Assertions to Better Specify the Amazon Bug
Web アプリケーションでブラウザの Back ボタンで戻って submit すると画面に見えてるのと実際に送信されるデータが異なる可能性があるからどうにかしたいよね、という論文。ちょっと古いから今もそのまま当てはまるかは不明。論文で書かれてるのは、設計レベルで assert として表示と裏で送るのが同じであることを記述しましょう、ということだけ。実装の話は何もないけど難しいのはむしろ実装だろうと思う。
author="L. Baresi and G. Denaro and L. Mainetti and P. Paolini",
title="{Assertions to Better Specify the Amazon Bug}",
booktitle="SEKE'02",
publisher="ACM Press",
pages="585--592",
year="2002"
本
クラウド ― グーグルの次世代戦略で読み解く2015年のIT産業地図、小池良次 著、インプレスR&D
読了。微妙。技術的にはクラウドと関係ない、あるいはクラウドである必然性のない話もいろいろ出てきていまいち。こういう本を読むと「クラウド」ってまだバズワードかなという印象。サービスの利用者にしてみれば、必要なサービスが適切なコストで利用できればいいわけでクラウドで提供されてるかはどうでもいい。サービスの提供側にとっては大きく変わるだろうけど、その辺がまだあまり区別されてないのかなという感じがする。
キーボード
HHK は x の下に Alt キーではなくて半角/全角キーがあって Emacs が使いにくくて仕方ないので AutoHotkeyの Remap 機能を使って Alt キーに割り当て。IME の on/off は Ctrl+\ にしてるから困らないし。設定ファイルは sc029::LAlt と一行書くだけ。
Efficient Type Inference for Secure Information Flow
制約解消ではない方法で型推論を行うという論文。やり方としては、型付け規則を Datalog という論理型言語に基づくデータベースクエリ言語で記述するというのが中心。あとは効率の良いアルゴリズムの話ばかり。
author="Katia Hristova and Tom Rothamel and Yanhong A. Liu and Scott D. Stoller",
title="{Efficient Type Inference for Secure Information Flow}",
booktitle="PLAS'06",
publisher="ACM Press",
pages="85--94",
year="2006"
Explaining Type Errors In Polymorphic Languages
前読んだ論文の発展みたいな論文。プログラム中の各構文要素(あるいは構文木の各ノード)がなぜその型を持っているか、型変数の値はなぜその値になったのか、といった説明文を生成する。何をやってくれるかは何となくわかるけど、どうやってるかは不明。
author="Mike Beaven and Ryan Stansifer",
title="{Explaining Type Errors In Polymorphic Languages}",
journal="ACM Letters on Programming Languages and Systems",
volumn="2",
number="1-4",
pages="17--30",
year="1993"
Finding the Source of Type Errors
型エラーの原因を見つける手法の提案。ちょっと古い。手法としては、単一化する際に型変数の値が決まればその理由を記録するというもの。理由って何かとか細かいことは全然書かれていない。
author="Mitchell Wand",
title="{Finding the Source of Type Errors}",
booktitle="POPL'86",
publisher="ACM",
pages="38--43",
year="1986"
ことえり
Mac を使うようになって半年くらい経ってそれなりに不満もなく使ってるけど、どうにもストレスなのがことえり。MS-IME は「頭悪いなぁ」とか言いながらもそれなりに学習もするし ATOK にしようかと思いながらも使い続けてるけど、ことえりは MS-IME とも比較にならないほど変換がおかしくて日本語入力が苦痛。ついでに操作性もよくないし。Canna でもここまでストレスにならなかったような…。ということで ATOK の導入を検討中。今すぐ買うなら 2008 for Mac だけど、2009 for Mac のベータテストが始まってるらしいからもう少し待つかどうするか。
Type Error Slicing in Implicitly Typed Higher-Order Languages
型付けに失敗した時にその原因箇所をスライスする手法の論文。 型推論は制約解消なので初めに解くべき制約集合を求める。この時、各制約とプログラム断片を対応付けておく。これにより、制約集合が充足不能だった場合に充足不能な極小部分集合を求め、極小部分集合に含まれる制約に対応づけられたプログラム断片をスライスとして得ることができる。この論文が対象としているのは let 付きの型付きλ。得られたスライスがやはり型付けできないことと、最小のスライスになっていることがちゃんと証明されている。
author="Christian Haack and J.B. Wells",
title="{Type Error Slicing in Implicitly Typed Higher-Order Languages}",
journal="Science of Computer Programming",
volumn="50",
number="1-3",
pages="189--224",
year="2004"
TeXclip
TeX で数式を書いて画像を生成するサービス。一応 Mac + Firefox で生成して、VMware Fusion + Windows XP + PowerPoint 2007 のスライドに貼付けられるところまで確認。¥ と \ を区別するみたいで少しはまりました。\ を使いましょう。
ML
今まで POP でローカルに取り込んでいた ML 系のメールを全部 Gmail に放り込むことに。とりあえず転送設定をして、ローカルのメールを全部 Gmail にコピー。なんかコピーできないメールが 2 つあったけど適当に回避。4 万くらいあったから結構時間がかかりました。
コメント
このブログはコメントが付けられますが、こちらで確認してから反映するようにしています。何日も気付かないことがたまにありますが、そんな時は気長にお待ちくださいませ。
追記(2009/05/08 08:27)
訂正です。ある条件を満たすと確認なしで表示されます。
Tractable Constraints in Finite Semilattices
有限な meet-semilattice 上の制約解消問題のうち真っ当に解ける(NP-hard でない)問題のクラスについて議論した論文。これを読んだのは、情報流解析の型システムを制約解消系として実装する時に解ける方に入ることを確認するため。似たようなことをやってる別の論文でこれに基づいているのがあるから大丈夫なんだろうけど、元論文にも一応当たっておくということで。
author="Jakob Rehof and Torben Æ. Mogensen",
title="{Tractable Constraints in Finite Semilattices}",
journal="Science of Computer Programming",
volumn="35",
number="2",
pages="191--221",
year="1999"