■

よく晴れる、初夏の陽気。起床は9時、出勤して論文書き。16時からテレビ会議、Agdaの新機能について。それからKtさんとCoqの話をする。また、帰納的定義のパースエラーの話の続報について教えていただく（実は論文の当初案が正しかった事が判明・・・今からもとに戻すべきだろうか）。
20時半に退所するが、阪急線が自己のため帰宅が遅れる。帰宅は22時半、夕食は麻婆豆腐。