AIM8が
本日開幕。午前は講演。
- 開発者による新機能紹介（パターンマッチングをソフトウェアレベルで実現、これは "Agda in Agda" を目指す一歩と考えていいんだろうか？）、
- "The power of Pi"（Wouter Swiersta)：依存型理論を売り込むためにはどうしたら良いか、というセールスを考えよう、データベースを扱うのに非常に適していると言えるんじゃないのか、という話。今、応募中のプロジェクトはまさにそういう話なので、非常に参考になりました。論文はこちら。
- "`Mugda', a small dependently typed language with type-based termination"(Andreas Abel)：Agdaの停止判定機構の作者による、新しい停止判定機構の提案。これまでのようなグラフ/辞書的順序ではなく、順序数上の帰納法みたいな方向を目指すそうです。
昼食は faculty clubで。白身魚のクリームソースがけご飯。美味。外国の何がいいかって、昼からビールを飲んでも、何も言われないところだ。
午後も講演。
