読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

PPL2008に行ってきた。

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


驚いたこと

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

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

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