コードスプリント（二日目）

起床は7時、出勤してコードスプリント。様相論理システムの第一バージョンが完成、昼のミーティングで一部発表する。いろいろ突っ込まれる、要改善。
午後は講演会、H氏の話（項書き換え系におけるTerminasionを多項式によってinterpretationする）は面白かったが2/3まで来て力つきる。他に開発者自身によるAgda2のパターンマッチ機能の紹介とか。
18時から懇親会、英会話でへろへろ、訳の分からないことを言って申し訳ないです。22時半に帰宅。