与

中洲のスナック。割と適当に入ったのだが

　年配のママが一人でやってるお店、35年だって

で、しばらく唄って帰ったんですが、まわりは、お兄ちゃんとおかまさんのお店ばっかりだったらしい

危なすぎる。いや、盛り塩してあったので、そこに入ったのが正解だったらしい

九州大学

伊都キャンパスのガイ∙ ダニエルと話してきました

プレゼンする見たいな話は、じゃかんすれ違いがあってなかったことに。まぁ、あんまりやりたくなかったのかも

実際あってみると「日本語は簡単なものだけ」ってことで、英語で話すことに

いや、日本人の奥さんなのに? まぁ、問題はない

関数型言語 Maude の話とか、その上の定理証明系の話をするんだが、Curry Howard 対応じゃないのか

どうも彼がいうには

　代数的プログラミングと、論理系(Curry Howard対応)は異なる

って話でさ。ふーん。いや、それは関係ないだろって僕は思ったが

なんか、モデルベースのForcingもやってるんだが、そんなこんなでずれがあって。まぁ、それが面白い

ZF/ZFC の話もしたんだけど、割とずれてたみたい

もともと JAISTの学生だったのね。まぁ、いろいろ楽しかった

まだ、しばらくは博多にいます

来週は博多

なんか、九大の先生とお話にいきます。火曜日から金曜日(2/24-2/27)

別に仕事というわけでもないのだが、なんか、プレゼンはするらしい

真栄原公民館

なんか、奥が工事されてて更地に

ってことは、裏から抜けられる! ということで、若干、近道可能に

なんか、そのあたり、道になりそうな気もするが、まぁ、だいぶ先だろう

あと、意味のわからない看板シリーズ

閃光のハサウェイ

いや、前作見てなくて。一応、最初に「前作は」みたいなのがくっついているんだが、よくわからんまま

まぁ、でも、見てても同じだろうな

女の子がからむと、こんな感じでしょ的な話でもある。でも、そこに予知能力みたいなのいれるの?

あんまりよろしくない。まわりがちやほやするのも含めて

絵がきれいってのは、そうだったかも。戦闘シーンのぴこんぴこんも、まぁ、それっぽいかな

桜

風邪ひいてたり、寒かったりで、あんまり桜はみなかったんだけど、今日は

　暑い。天気がよい

なので、結構、桜をみました

agda 2.9 の続き

% agda --version
Agda version 2.8.0

% ~/.local/bin/agda --version
Agda version 2.9.0

agda Sheaf.agda 410.01s user 3.28s system 99% cpu 6:54.04 total
~/.local/bin/agda Sheaf.agda 342.05s user 2.26s system 99% cpu 5:44.73 total
~/.local/bin/agda -j7 Sheaf.agda 574.62s user 93.03s system 117% cpu 9:27.13 total

これは、並列処理すると遅くなる感じ。でも、新しい方が、ちょっと速いのか

~/.local/bin/agda --warning=UnusedImports Sheaf.agda

これは、一応、動いているらしい