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

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

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