せっかくさくらのサーバーを借りているので、ブログもあっちに移すことにした。 というわけで、以後記事はそっちに書くことにする。 ただ、インポートがうまくいかなかった関係でこっちのデータは当面残すことにした。 なんだかなあ。

東工大にいること10年、学生を始めて22年、無事博士号（工学）を取得し、学位記授与式に出席しました。 写真は撮ってません。 アカデミックガウンは着ました。 写真は秘密です。 思い返せばいろんな転機がありましたが、ここでは話さないことにしましょう。 …

ポルトガルに出張に来たので（まだいる）VodafoneのSIMを買った。 もともとの予定ではMifiか何かを借りる予定だったのだけど、うっかりしていて予約を忘れていた。 この引きこもりでさえ買えるのだから、まあありがたい限りだ。 空港なら英語が結構通用する…

おわったはず。 まだこまごまとやることあるけど。 少し頻度上げて書きたいな。 これからたぶんAgdaやることになるし、そのメモとか。

今年に入って何も書いてないじゃないか。 まあ、もう少しで一段落つくのでそこで少し書きたいな。

デザインを変えた。 白い。 まあ白い方がいいかなあ、なんて。

ML/LL Advent Calendarのネタとしてはいくつか思いついたものがあって、 Linear Logic Linear Lisp（別のAdvent Calendarで出たようなので避けて賢明か） Module Type（Coqの） Moonlit Lo...げふんげふん なんだったか忘れたね。

これが最後の学期になりそうだ。

最後の学生生活。 ・・・最後だといいなあ。 うん、最後にしよう。

ときどきTwitterで出てくる「言葉狩り」という現象についてちょっと気になったので書いている。 言葉狩りといっても、ある特定の語を禁止し、別の言葉に言い換えてしまうことがほとんどなのだが*1。 いわゆる差別用語とか、特定の侮蔑とか、言いにくいが児ポ…

一応生存を主張。 この間、論文を書いて、終わってへばって、次の論文に向けていろいろ考え中。 アイディアは大体固まったので、もう少し詰めてからやってみるかな、という感じ。 Coqのサブセットもその一つ。 まあ、Notationないけどね！ Typeもないけどね…

Round 1Aについて。 今度はA,B,Cの三問。 前回と同じく、最後だけ解けなかった。 解けた問題だけとりあえず解説。 A パスワード入力画面で、すでに何文字か打ったが、ある時点で間違ってしまったかもしれない。 これから何文字か削除して再開するか、それと…

GCJ = Google Code Jam。Googleがやってるプログラミングコンテスト。 アカウントはちょこちょこいろんなプログラミングコンテストに登録しているのだが、まともにやったのは今回が始めて。 Qualification roundとRound 1aが終わって、とりあえずRound 2には…

少しメモ書き程度に。 研究の展望があるのに、それを実装するコストがとんでもないことに気付いた。 並列計算について少し調べたいな。並行もだけど、並列はどうなんだろう？ そういえばC言語超入門とかいうよくわからないものもあったっけ。 Coqのテキスト…

今b-mobileのSIMで使っていて、パケットを使いたくなかったのでDoCoMoショップに行ってみた。 聞いてみたところ、アップデートさせてくれるということで、SIMを持ってきてくれて、相手の目の前でアップデート。 無事できた。よかった。 と思ってたよ今日まで…

Theorem Provingのアドベントカレンダーに参加しようと思ったのだが、現時点で参加者5人。 このままだとどうなるのだろうか・・・？ できれば参加者求む。

パワポを共有・・・というよりアップロードするサービスがあったので、アップロードしてみた。 内容は去年の夏ゼミで話したCartesian Closed Categoryの話。 もちろん（と言っていいか疑問だが）日本語。 Cartesian Closed Category View more presentations…

なんか今朝アクセスポイントの設定がおかしくなっていた。 テザリングをした影響か？ ちなみに普通にアクセスポイントの設定を直したら直った。

b-mobileでのテザリングができないという話を聞いたのだが、今日試したところできた。 ちなみにSIMロック解除済み。それが影響しているかは不明。 今これを書くために使っている回線がテザリング。

終わった。 まだいろいろ続くが、とりあえず一段落。 ・・・でも、昨日まで書いてたやつはまだ修正しないとな。

直近のタスクがあと一つ。 それが終われば少しは休み気分・・・ なんて暇はあったっけ・・・？

なりましたので、思いついたことがあってもここに書けません。 そのうちそのうち。

昨晩寝ようと思ったときに、ふとどこぞのブログで無限がどうこう、という話があったな、と思い出した。 少し考えてしまったおかげで寝るのが遅くなったのだが・・・ というわけで、少し考えてみる。 有限の大きさ 1個のお菓子が入った袋と2個のお菓子が入っ…

オワタ！しないですんだ。 よかったよかった。 でもキューにはまだまだたくさん詰まってるのでしたとさ・・・

とりあえず4月1日になったようだ。 学生たちの卒業、新社会人の誕生、といいことの中で。 エイプリルフールか。 としか思わなくなっている自分が。 まあそんなものだろう。 うまくしかけられる人間になりたいものだが・・・

今日帰るはずの出張で札幌にいました。 バスの中で停車中に横にゆれたもので、「そんな馬鹿な」というレベルの印象。 そして飛行機は飛ばない。 飛ぶかと思っていたが、そんな甘いわけもなく。 ひとまず家の状況が気にはなるが、一泊延長し、明日帰る予定で…

これから、本当にほとんどの人には興味が向かないような、その上わけがわからない記事を書く。 なので、CoqやHaskellが好きな方以外はあまり見ないことをお勧めしておきたい。 ・・・などと、こんな記事を書いて自分も何をしたいのやら。

大晦日となりました。 今年は研究の方針を変えた。 そのくらいしか思いつかない。 来年は卒業できるかが決まる。 あ〜あ・・・できるのかねえ。

法治。じゃない、放置。 いけないいけない。多少はしっかり書かなければまたものぐさになってしまう。とりあえず、まだ生きてる。 元気に。 多分。 Twitter見たほうが早いけど。

一昨日（表示は昨日になるかもしれない）、Coqのサブセットを作ろうかな、と書いた。 でもサブセットってどのくらいよ？という問題が出てくる。 少し考えてみよう。 まず、Coqのサポートしている範囲を挙げる。 言語について：Vernacular（コマンド用言語、…