こちら。intruderさんとは、若手フォーラムのワークショップで共同発表をしたりしました。曖昧性や集合論に関する、日本でも数少ない同業者だっただけに、とても残念です。

晴れているが寒く、風が強い。起床は9時半、気の滅入る一日。出勤する途中はお天気雨に降られ、電車は逃し、図書館は休刊日、などなど。ついでに、年度末、本日付けで辞職される方々の挨拶メールの量にさらに気が滅入る。職場ではAgdaを最新版にアップデート…