[Coq] Proof Cafe #01

Proof Cafe (栄)に参加しました。

　当日使われた資料はyoshihiro503の日記を参照の事。

　yoshihiro503さんによるCoq最速文法マスターという感じで、僅か90分の入門講座で、（Haskellなど関数型言語の知識があるとはいえ）Coqに初めての人が
Theorem append_length : forall (A: Type) (xs ys: list A),
length (xs ++ ys) = length xs + length ys.
を証明出来る様になるってのは、やはり説明の手際が良いよなぁ。次に入門用PPTを修正する時は是非とも参考にしよう。

　Proof Cafe自体は２時間だったんですが、その後、懇親会を実施して頂き、なんか身に余る様な歓待をして頂きました。皆さんどうもありがとうございました。Coqに限らず関数型言語とかIT業界の話とか色々楽しく話をしました。

　Proof Cafeは今後も毎月名古屋で開催されるとか、Proof CafeでもCPDTを読もうとしている、ようです。Formal Methods Forumの方でも頑張ってCPDTを読んでいきたいです。