PPL2008に行ってきた。

Coqでπ計算などで有名なReynald Affeldtさんから、貴重な意見がいただけたり、楽しい話がたくさんあったりで、非常に素晴らしい経験だった。

驚いたこと

• プログラミング in OCamlでも有名な五十嵐先生のところの研究室では、CALと呼ばれる、小さい証明器を使って、学生に論理学の勉強をさせているそうだ。

Coqのようなtacticや、豊富なライブラリがないということなので、確かにCALで証明できれば、論理学が、より理解できそう。

• プログラミングの基礎などで、有名な浅井先生は、今年度から学部生向けにCoqの講義をしているそうだ。

浅井研のB4の学生が、夏からCoqをさわって、1200行ほどもあるコードを読んで、拡張して、1500行くらいのコードを買いて、発表していた。恐るべし、浅井研究室。