今日は勉強会

今日は久しぶりの勉強会でした。

まずは id:suer さんによる、 PPL Summer School のレポートでした。SAT Solver が超速い！みたいな。問題の制約を SAT の形式(?)にエンコードできれば、すごい速さで問題を解くことができるそうです。すげーな。
次は id:yoshihiro503 さんによる、Coq 入門でした。Coq で関数を定義して証明してくれました。そのあと"Curry-Howardの対応を知らない子ども達"を読んで、素直に感心しておられました。