ちなみに最近のXavier Leroy（OCamlの作者）の余帰納的定義による操作的意味論はさらによさげ。まだほとんど読んでませんが、99%推測でいうと「small-step semanticsより簡潔だが、無限ループとエラーを区別できなかった」（区別するのが面倒だった）big-ste…

のために今日も正式に有給ですよ（←強調）。まだおかゆとうどんしか食べられないし。暇なんだけど、家の中を立って歩いたり、PCに長く向かってると、やっぱりちょっと気持ち悪い…

意味論の勝ち組は明らかに操作的意味論かと。:-) 仮想機械による実行で定義していた頃は「汚い」とか言われましたが、small-stepにせよbig-stepにせよ、ただの帰納的定義で済むことがわかってしまったので。（参考：Types and Programming Languagesの3.4節…

も入ってた（地上デジタル放送だけでなく）。半年間、気づかず。体調が回復したら、分配器を買ってこよう…

∃は抽象型（abstract type）にあたります。とか超遅レス。∃α．τは「ある型αが存在して、αについては、型τの値（関数など）が利用できる」ということなので。とっくに解決してそうですが。あと、型を値の集合とみなすこと自体はOKなのですが（というかイデア…

金曜から下痢と嘔吐が…。少し良くなってきましたが。ウィルス性急性胃腸炎だそうで、水を飲んでも吐いてたので（今はOK）、点滴＆注射しまくりでした。もし僕だけじゃなくて他にもいたら、また食中毒？（前にも某試験関係のお弁当で当たった。そのときはみん…

「AIBOでOCamlを動かせないか（＝OCamlでAIBOを動かせないか）」という話で、AIBOのCPUは"ARM MIPS R?000"みたく聞いたのですが、そういうCPUがあるんでしょうか？ ARMとMIPSは別のCPUだと思ってた…。ちょっと検索しても仕様は「64ビットRISCプロセッサ」と…

メール＆書類処理 またMewの不調と格闘。やはりEmacsというかDebianをアップデートするしかないのか？ ↓に備えてノートPCのアップデート（この間のノートPCとは別） ３時間耐久会議＋忘年会 うーん、本当に研究していない。今日の午前はなにをやっていたんだ…

というスライドを教えてもらった。プログラミング言語研究も悲惨です。PLDIなど、まさに←に書いてある通り。POPLやICFPはまだマシだと思うのですが、命令型言語の「研究」者や開発者には（ほとんど）無視されてるし。

書き損なった。 IEとかウィルス対策ソフトウェアとかVMwareの仮想ディスクとかをアップデート（フォーマット変換）したら２時間ぐらいかかった。遅。;_; 講演会＆懇親会 その合間に創造工学研修。今日は（今日も？）ちゃんと対応できなくてスミマセン…

他のトラックバックを見ると、やっぱり勘違いしている人が…。「（制御をのっとられるような）いわゆるバッファオーバーフローではないのでヨロシク」という発表です。「バッファオーバーフローを認めた」というのはCNetの間違い（少なくとも今のところは）。…

饋還。そもそも読めませんでしたが。僕は電気系じゃないので（言い訳）。Wnn6では変換できたのですがMS-IMEでは（略）←しつこい

http://japan.cnet.com/news/media/story/0,2000047715,20092716,00.htm http://news.com.com/2100-1002_3-5992215.html元記事が50%ぐらい間違いとすると、日本版は95%ぐらい間違いのような。いや、数字は適当ですが。P.S. 無謀にもトラックバックしてみる。

MinCamlのescape解析のstore typing修正。 会議。2時間。 4日連続忘年会1日目。ネクタイ率が極めて高くて場違い。やはり工学系＆電気系。;_; 全然研究してない…

今朝出勤しようとしたら、車が凍っていたのでお湯をかけて溶かしました（本当）。正確には、凍ったのは車じゃなくてフロントガラスに積もった雪ですが。ぬー。

インストールの続き。細かいカスタマイズとか、on demandに。WordやPowerPointのオートコレクトをすべてオフにするとか。 某会議のために議事録のとり方というか書記係のやり方についてマニュアル本や前例を調査(?)。「…と決定」みたく体言止めにしたのだが…

ということで、予算申請とか研究紹介の資料に利用すべく、社会的問題になった有名不具合(?)の収集を開始。タイトルが「社会的不具合」のエントリに今後追加していくということで。古いものから新しいものまで、思いつくだけでも山ほどありますが、まずは み…

Firefox 1.5がバッファオーバーフローしてのっとられるというのはガセだったようです。一応。

ちなみにPennとかアメリカの私立大学は、学部生の授業料がものすごい金額なので注意。大学院生は（まっとうな大学＆学科では）タダというか、給料をもらえますが。でも、ボスの予算が尽きたり研究が進まないとクビ。

やっぱり(?)システムのバグもあったそうで。内容がよくわからないので、検証できたかどうか（笑）わかりませんが。とか後からいってると、かえって（ますます?）形式的手法のイメージが悪くなりそうだが。

某予算の関係で「なんで日本は欧米より情報教育のレベルが低いのか」みたいな話になったのですが（ここではレベルが低いことは明らかな事実とし議論しません。もちろん、多少の例外はあります）、僕は突き詰めると 言葉の壁 距離の壁 の2点に尽きると思いま…

どうも音量が安定しないんですが、臨場感演出のため？ 某ワイドショーで急に声が大きくなり、ビックリしてまさに「目が覚め」たり。あと、某石油ファンヒーターの欠陥アナウンスも、モゴモゴと何を言っているのかわかりません。僕が年寄りだから耳が遠いだけ…

半年で10%以上の消費。このペースだと5年ともたない計算に…。やっぱり2GBや3GBじゃ足りないと思います。いや本気で。Gmailを使い始める前も合わせると、すでに10GBぐらいあるし。

片山さつきさんは５人目だったそうで。うちの親は１．５人目（２人同時）だったようですが結婚退職。もったいないのか、良かったのか…？

いつもの人がいつものようにS/N比を超下げまくってるなー、とか思ってたら、Rossbergがツッコミを入れていた。まじめだ。解説：unitは属する値が一つしかない型で、「特に返り値がない」関数の返り値の型。あと、「特に引数がない」関数の引数の型。それに対…

故障したHDDを交換しにDellの人が来た。アポが10時だと思ってて諸般の事情により（謎）遅れて慌てたが実は11時だったらしい。いよいよ痴呆進行中か。;_; 修理の横でMinCamlのエスケープ解析（僕じゃなくてTAの人のアイディア）の健全性証明について考える。…

これは検証しても駄目だなあ（当たり前）。構造計算結果偽造のニュースのときは、誰でも「電子署名しろよ！」って思っただろうけど…

配属希望の分析＆反省;_; メインのマシンがまたハング→頻繁なのでDELLのサポートに電話→HDD故障判明→バックアップとか;_;;_;（明日の10時に修理がくる） ゼミ：shape analysisのお話を聞く 修士学生さんのミーティング×２

前から怪しかったのだが、一日一回ぐらいハングしはじめたので、またDellに電話して診断テストをやったらHDD故障だった。;_; バックアップやら再インストールやら頭が痛い。下らない雑用ばかり増えて研究ができない〜

忘年会費や親睦会費がすごい金額で馬鹿になりません。今月だけでｎ万円（ｎ＞３）。酒が飲めない＆旅行などもほとんど参加できないので、丸損です。ぬー。