英語の論文の続き。外は明るいけれど気がついたら20時半。最後に残っていたNも帰るというので慌てて帰る。Jarntorgtの広場にあるパブで夕食。 テラスでビールを飲むにはいい気温。これで夜の21時半。熱気球も飛んでいる。 チェコビールとパスタ。

今後のAgdaの方針を決める討議、本日はUniverse Polymorphismに関して。 Agdaはご存知の通り、非常に厳格なpredicativityに基づいていますが、しかし厳格な可述性は、しばしばデータ型を定義する際の面倒の元になります。例えば record Cat: Set1 where Obj:…

開始は9時半から。 本日の講演は "A Tool for Automated Theorem Proving in Agda" (Fredrik Lindblad)のみ。定理の自動証明の効率化を図るツールをAgdaに実装する話。すみません、よく覚えていません、はい。

今日も晴れ。起床は7時、体調は良好だが咳は止まらず。 朝ご飯。バイキング形式で、シル（白身魚の酢漬け）が美味。