バースと同じ内容を45分で発表。出来は、えーと、6回投げて8失点という感じ、散々でした。突っ込まれたポイントは
- 実装の対象となった様相論理の体系がなじみがなく、直感的な理解が難しい
- Agdaの停止判定機構に関する私の説明に、一部、Agda ver.1 そのままの説明が混じっている
- 私の講演の論旨は「様相論理の充足関数を実装しようとして、それが定義そのままの実装では停止判定に合格しないので、様相論理の論理式のデータ型を増やすことで停止判定に合格した」であるが、しかし合格したのは関数定義内部でスタッキングをしたからで、論理式のデータ型の変更はそのスタッキングをし易くするものの、データ型を増やしたおかげで合格した訳ではない。つまり型の変更は必然的ではなかった。
という点でした。当たり前の話ですが、専門家恐るべし。よっぽど消沈（笑）していたのか、終了後、所長とD先生にわざわざ慰めに来ていただきました。ありがとうございます。
その後昼食。今度は「アインシュタイン・カフェ」とかいう学内のカフェテリア（実はアインシュタインとは何のゆかりもないらしい）に行く。院生のS氏と昼食を食べながら雑談。
