http://www.cis.upenn.edu/~plclub/popl08-tutorial/POPLに併設されていたので参加しました。CoqでTAPL序盤（単純型つきλ計算まで）の理論を定義・証明する、という内容。主催者（PennのPLClubの人たち）に聞いたら、先週金曜のカウントで参加登録者67名との…