Coq'Art読書会あらためSF読む会 2013年10月06日

「Coq'Art読書会あらためSF読む会」に参加してきました。

Coq'Art読書会あらためSF読む会 #1 #readcoqart - PARTAKE

最初『Coq'Art』という本を読む予定だったらしいのですが、まずもっと初歩的な『ソフトウェアの基礎』を読む勉強会になったようです。 僕はCoqを全然知らないので『Coq'Art』を読むのは厳しいかなあと思って二の足を踏んでいたのですが、『ソフトウェアの基礎』は僕でも理解できそうかなと思って参加することにしました。

この『ソフトウェアの基礎』ですが、大変素晴らしいテキストですね。

sfja/sfja

元のテキストが非常に初歩的なところからやってくれているのに加えて、名古屋方面の方が翻訳されており、とても読みやすかったです。 Coqに詳しい人が集まっているので、時折入る解説も大変参考になりました。 今回は Basics_J.v の3分の2くらいをやりました。データ型と関数の定義の仕方、destruct、inductionを使った証明あたりまで。

Proof Generalも簡単な操作はすぐに覚えられました。 ただ、ddskkとccc.elというファイル名がかぶっているらしく、同時に読み込むとエラーになりました。 たぶんCoqを使うだけならccc.elは使わないと思うので削除して対応しました。

僕みたいにCoqが全然わからない人でも参加できる勉強会だと思うので、参加してみるといいと思います。