<< 4月 2009 | ホーム | 6月 2009 >>

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"

http://doi.acm.org/10.1145/568760.568863

タグ : ,

クラウド ― グーグルの次世代戦略で読み解く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"

http://doi.acm.org/10.1145/1134744.1134759

タグ : ,

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"

http://doi.acm.org/10.1145/176454.176460

タグ : ,

ビューティフル・マインド、Sylvia Nasar 著、塩川優 訳、 新潮社

読了。J.F.Nash の伝記。

タグ :

めも

WebDriver

タグ :

オープンシステムサイエンス、所眞理雄 編著訳、NTT出版

読了。ソニー CSL の研究。

タグ :

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"

http://doi.acm.org/10.1145/512644.512648

タグ : ,

ストリング理論は科学か、Peter Woit 著、松浦俊輔 訳、青土社

読了。

タグ :

休み

今日から一週間休校になりました。休講になるだけでそれ以外は普通に仕事ですが。ただ、食堂も購買も全部休みになるので食事に困ります。いつも昼と夜は食堂なのに。

タグ :

ことえり

Mac を使うようになって半年くらい経ってそれなりに不満もなく使ってるけど、どうにもストレスなのがことえり。MS-IME は「頭悪いなぁ」とか言いながらもそれなりに学習もするし ATOK にしようかと思いながらも使い続けてるけど、ことえりは MS-IME とも比較にならないほど変換がおかしくて日本語入力が苦痛。ついでに操作性もよくないし。Canna でもここまでストレスにならなかったような…。ということで ATOK の導入を検討中。今すぐ買うなら 2008 for Mac だけど、2009 for Mac のベータテストが始まってるらしいからもう少し待つかどうするか。

タグ :

ケプラー予想、George G. Szpiro 著、青木薫 訳、新潮社

読了。

タグ :

めも

phc -- the open source PHP compiler

タグ :

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

TeXclip

TeX で数式を書いて画像を生成するサービス。一応 Mac + Firefox で生成して、VMware Fusion + Windows XP + PowerPoint 2007 のスライドに貼付けられるところまで確認。¥ と \ を区別するみたいで少しはまりました。\ を使いましょう。

タグ :

宇宙をプログラムする宇宙、Seth Lloyd 著、水谷淳 訳、早川書房

読了。

タグ :

ML

今まで POP でローカルに取り込んでいた ML 系のメールを全部 Gmail に放り込むことに。とりあえず転送設定をして、ローカルのメールを全部 Gmail にコピー。なんかコピーできないメールが 2 つあったけど適当に回避。4 万くらいあったから結構時間がかかりました。

タグ :

利己的な遺伝子、Richard Dawkins 著、日高敏隆、岸由二、羽田節子、垂水雄二 訳、紀伊國屋書店

読了。

タグ :

資本主義と自由、Milton Friedman 著、村井章子 訳、日経BP

読了。

タグ :

コメント

このブログはコメントが付けられますが、こちらで確認してから反映するようにしています。何日も気付かないことがたまにありますが、そんな時は気長にお待ちくださいませ。

追記(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"

タグ : ,

風邪

金曜日の夜から体調不良で家でおとなしくしています。どこか走りにいこうと思ってたのに。風邪には気をつけましょう。明日は所用で名古屋に行きます。

タグ :

フォン・ノイマンの生涯、Norman Macrae 著、渡辺正、芦田みどり訳、朝日新聞社

読了。

タグ :