Privacy-Sensitive Information Flow with JML
JML を拡張して非干渉性に関する条件を書けるようにしましたという論文。Krakatoa と Why を使うと JML から Coq に落とせるから、Krakatoa も拡張して非干渉性を扱えるようにした。著者らの興味は privacy-aware なデータマイニングらしく、Naive Bayes Classifier の非干渉性に対する JML が示されている。
author="Guillaume Dufay and Amy Felty and Stan Matwin",
title="{Privacy-Sensitive Information Flow with JML}",
booktitle="CADE 2005",
publisher="Springer",
volume="3632",
series="LNCS",
pages="116--130",
year="2005"
本
- なぜビッグバンは起こったか : インフレーション理論が解明した宇宙の起源
- Guth, Alan H, 1947-，林, 一, 1933-，林, 大, 1967- 著
- 早川書房
読了。
ドライブ
リフレッシュ目的でドライブ。今日は珍しく東の方に行こうということで静岡に踏み込むことに。実家にいた頃も行ったことないはず。ルートをあまり考えずに出たので浜名湖 SA でどう回って帰るか悩む。しかも、高速にのる前に買い物で手間取って思ったより遅くなってたし。ということで、結局いつも通り道の駅を回ることに。花桃の里と横川。時間があればくんまとか鳳来とかも行けたような気がするけど、今回はちょっと時間調整に失敗。帰りに伊勢湾岸道から見えた名古屋港の夜景は結構いい。車を停めて見れる場所がないけど。今日の走行距離は 500km 弱。今度は愛知と静岡の県境あたりを回るとか、それとも御前崎あたりまで行ってみるとかいいかも。
ようやくナビの曲がる交差点の案内に慣れてきたかも。右折の場合、700m先右方向、300m先右方向、まもなく右方向、右方向、なんだけど、最後のがあまりにも直前過ぎて何度か通り過ぎたことがある。ナビは便利だけど、事前に地図を見てちゃんとルートを覚えなくなったから走ろうと思ってるルートを外すことがあってそれがよくない。ナビだと細かいルート設定するの面倒だし。
最近は長距離運転だと右足がつりそうになることがあってよくないんだけど、今回は 8 割くらいが高速道路ということでクルーズコントロールが活躍。ペダルを踏まなくていいからかなり楽。変な加減速をしなくなるから燃費ものびるし。あと、前の車よりパワーがあってシフトダウンして踏めばポンと加速できるから、余裕を持って運転できるのも楽。