昨日のドライブまとめ。もとの予定ではもっと西のほうに行くつもりだったけど、宝塚あたりの渋滞が嫌で紀伊半島を反時計回りにぐるっと回ることに。阪和道の南端まで行って、海沿いの 42 号を走って、紀勢道で帰るルート。行きの下津辺りと帰りの亀山辺りの渋滞で 2,3 時間ロスした感じで、結局渋滞は避けられず。いつも通りちょくちょく道の駅に寄りながら移動。すさみの辺りでオート三輪とすれ違ってびっくりした。子供の頃に 1,2 回見たことがあるくらいで、今でも走ってるとは思わなかった。昨日の走行距離は 580km 程度。渋滞で左足がしんどかった。もとの予定だったところは休日 1000 円のうちに行くつもり。

コメント追加

投稿者 kw : 2010年5月4日 11:26:00 JST #

並行プログラムを対象とする情報流解析の型システムが非干渉性に対して健全であることを Isabelle/HOL を使って示したという論文。逐次プログラムの非干渉性は、高機密度のデータのみが異なる初期状態から実行した結果が区別できないことだけど、並行プログラムの場合は利アクティブ性を考慮して bisimilarity を要求する。それと、スケジューリングの方法によって実行が変わるのでスケジューラを考慮できるようにする。というセッティングのもとで健全性を証明。

author="Gilles Barthe and Leonor Prensa Nieto",
title="{Formally Verifying Information Flow Type Systems for Cuncurrent and Thread Systems}",
booktitle="FMSE '04",
publisher="ACM",
pages="13--22",
year="2004"

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

コメント追加

投稿者 kw : 2010年5月2日 13:49:00 JST #

読了。

コメント追加

投稿者 kw : 2010年5月1日 18:28:00 JST #

今週は研究室のネットワークが不調で、それの面倒を見るのに時間が取られました。つながったり切れたりを繰り返してたんだけど、結局ルータがおかしくなっていたようで、別のものに交換したら切れることはなくなった模様。ただ、それ以外にも予想と違う挙動をいろいろ見せられて疲れました。とりあえず、全容を把握している人間が誰もいないのは問題ですな。

コメント追加

投稿者 kw : 2010年4月30日 22:05:00 JST #

明日は所用につき日帰りで帰省。車が変わって ETC を付けたから、高速道路が使いやすくなってちょっとは楽。

コメント追加

投稿者 kw : 2010年4月24日 22:31:00 JST #

Haskell 本は 2 冊持っているつもりでいたら、実は 3 冊だった。引っ越した時の箱の中に埋もれているのを今日発見。いつ買ったのかとか、一通り読んだのかとか、全然記憶がない。持っている技術書の類は本棚.orgに登録してるけど、探したらあるし。

コメント追加

投稿者 kw : 2010年4月24日 22:24:00 JST #

読了。珍しく練習問題もある程度やってみた。

コメント追加

投稿者 kw : 2010年4月16日 21:47:00 JST #