以前、ドーソンの「ロジカル・ディレンマ」の日本語版について当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分に大学へ、誰もいなくて鍵を開けてもらうまで少し待つ。