20時から市内のジャズバーで参加者の親睦会、ラテン音楽の夕べ。市内観光で疲れていたのか、最前列で寝ていたのは秘密だ。 バーの近くの大学の駐輪場にて。A君曰く、「これぞヨーロッパ」、何をしても自転車は盗まれる。

それから海辺でビール。 陽光が眩しい。 市内、川はかつての市城の掘り割りだったらしい。

市内には各種艦船の展示コーナー MARITIMAN があり、いろいろな船があった。 スウェーデン海軍の駆逐艦 HMS Smaland が非常に興味深かったので、写真を紹介する。 火器担当士官室。こんなところも北欧デザイン。

起床は8時。風邪は少し良くなったようだ。朝食をとり、午前はホテルで仕事。午後、市内観光に出かける。 港町。今日も雲一つない晴天。

以前、ドーソンの「ロジカル・ディレンマ」の日本語版について当Blogで紹介いたしましたが、渕野先生から本日、その件でメールをいただきました。先生は組み合わせ論的集合論における業績だけでなく、「巨大基数の集合論」（kanamori）の訳者としても知られ…

本日は班決め。私は、本日の発表について、英語の論文を書くことに。19時にみんなで退出、19時半から市中心部のレストランで夕食会。フランス料理、ビールと牛肉でお腹いっぱい。

"Using a logical theory of constructions for program verification" (Andreas Sicard)：コロンビアの大学の先生。講演のスライドはこちら、アブストラクトはこちら。 logical theory of constructions (LTC)上でgeneral recursive programs（停止しないプ…

バースと同じ内容を45分で発表。出来は、えーと、6回投げて8失点という感じ、散々でした。突っ込まれたポイントは 実装の対象となった様相論理の体系がなじみがなく、直感的な理解が難しい Agdaの停止判定機構に関する私の説明に、一部、Agda ver.1 そのまま…

開始は9時から。 "Formalization and test generation for a CPU architecture"：A君による発表。 "A Type of Partial Recursive Functions " (Ana Bove)：部分的帰納関数を型付けできるように、圏論を使って型を定義しようという話。面白かったです。対応す…

よく晴れた日、気温は20度を超える。しかし未だに咳が止まらない。起床は7時、もうすでに日は高い。ホテルで朝食。8時45分に大学へ、誰もいなくて鍵を開けてもらうまで少し待つ。

日本人組はみなN教授に招待され、お宅へ伺う。庭のテーブルで夕食。 茹でエビ。すばらしく美味しうございました。24時にホテルに帰る。

本日開幕。午前は講演。 開発者による新機能紹介（パターンマッチングをソフトウェアレベルで実現、これは "Agda in Agda" を目指す一歩と考えていいんだろうか？）、 "The power of Pi"（Wouter Swiersta)：依存型理論を売り込むためにはどうしたら良いか、…

起床は7時、ホテル食堂で朝食。トラムを乗り換えてC工科大へ。 画像は駅。 計算科学科の建物の最上階は「コーヒールーム」になっていて、カフェにあるようなエスプレッソマシンがあり、上画像のようなスペースもある。うらやましい。 そのテラス。風が心地よ…

起床は7時半、宿舎備え付けの紅茶とビスケットで朝食。8時のタクシーでブリストルへ。バース空港内のスタバでサンドイッチを食べる（イギリスのサンドイッチはどこもおいしい）。10時の便でアムステルダムへ（今度もよく揺れた）。空港で昼食（パニーニとビ…

市内で夕食会。P教授が引率して、6人で市内へ向かう。 途中にあった、ジョージ・オースティン（ジェーン・オースティンの父）の墓。 市内を歩く一行。 海鮮レストランに行き、夕食。私はタラを食べる。イギリスの魚は美味しい。

G氏と彼の学生とA君を交えてお茶を飲む。 （調整中）

その後は回復したA君と私が発表。45分のはずが30分になったので、大急ぎで終わらせる。和やかな雰囲気で終了。 驚いたのは、終わった後、わざわざG氏が握手に来たこと。お互い「出稼ぎ論理学者」なので、同種の臭いを嗅ぎ付けたんだろうか。

午後の発表は、所長による研究所の紹介と、Alessio Guglielmi氏による "deep inference" の紹介。 "deep inference"は、Girardによる"Gemoetry" から発達した証明論の技法の一つ*1で、「exchange ruleなどの官僚主義的な瑣末にとらわれることなく、contracti…

起床は7時半。発表練習をしてから、9時にP教授のオフィスに集合。午前中はB大学の人の発表を聞く。しかし寒くて震え上がり、とても発表を聞くどころではない。 昼食は大学のカフェテリア、カレーを食べる。同行していたA君の顔が真っ青で、気分が悪いらしく…

ロイヤル・クレッシェント。 夕食は市内のレストランで、ラムチョップを食べる。22時に帰宅、発表練習を途中までして寝る。

その後は市内観光。私は一人で、P教授のおすすめのバースのご当地作家ことジェーン・オースティンの博物館に行く。手違いでintroductly talkに二回出るが、解説する人によって内容が全然違う事に驚く。最初のおばさんは当時のバースの「結婚市場」の説明とジ…

起床は6時。ホテルのバイキングで朝食（ソーセージが良い）。9時15分（大陸時間）の飛行機でブリストルへ、9時半（イギリス時間）に到着。天候が悪く、かなり揺れた。 写真はスキポール空港。 イギリスはものすごい天気で、強風と大雨、気温は10度以下。さす…

特に事もなし。関空で他メンバーと合流、KLMでスキポール空港（アムステルダム）へ。ホテルはトランジット客用のもので、空港からバスが出ている。一回ホテルに行き、また空港に行ってバーで夕食。パスタとハイネケン。 スキポール空港。 オランダの公衆電話…

起床は6時15分、6時50分にM○タクシーを呼んであったのだが、いっこうに来ない。7時に電話をかけると、「手違いで予約が登録されていませんでした。代車も手配できません」・・・。慌ててスーツケースをかついで駅に向かう。坂をおりきったところで個人タクシ…

イギリスとスウェーデンに出張します。帰国は6月6日（金）の予定です。その間、当Blogも更新が出来ないかもしれません。ご了承ください。

強い雨、湿度も高い。風邪もぶり返し、咳が続く。 起床は10時半、発表練習をする。夕方、美容室へ行き、駅前の書店で本を買って帰宅。夕食はツナのトマトソースパスタ。 「今日の早川さん2」を読了。最後の話が、ちょっと感傷的すぎるような気もする。

晴れた日、気温も上昇。湿度は依然として高い。 起床は7時半、出勤して会議。その後発表準備、1時間半の予定で発表原稿を作っていたのだが、持ち時間が45分という事が判明したので、原稿を削る。退所間際に小飲み会があり、飲み屋によって、23時に帰宅。

本日始めて知ったこと。ゲーデルの本来の枠組みは（単純型理論を含む公理系であって）induction scheme も含む事。 "Proofs and Types"では単純型理論として紹介され、induction axiom は含んでいません。恥ずかしながら、これしか読んだ事ありませんでした。…

晴れ、湿度は依然として高い。ついでに、咳がまだ止まらない。 起床は9時半、出勤して会議と打ち合わせ。それから発表準備をする。帰宅は21時15分、夕食は肉じゃが。

晴れ、気温は凉しめ。強い咳は出るが、体温は平常に戻る。起床は9時半、出勤して発表準備の続き。何事もなく一日終了。帰宅は21時半、夕食は鶏肉のマスタードソースとジャガイモ。