こんにちは，@yu-i9 です．
今回はCAMPHOR- HOUSEで開催されていた Coq勉強会について報告します！
Coqとは
定理証明支援システムの一つで，カリー・ハワード同型対応に裏付けされたラムダ計算を用いた証明が特徴です．ざっくり言ってしまえばコンピュータ上で証明を行うためのシステムです．
経緯
発端は2015年の8月．もともとCoqに興味があった @yu-i9 と，話を聞いて興味を持った後輩（当時CAMPHOR-とのつながりはなかった）との間で勉強会をやろうという話が出ました．さらに，二人では寂しいということで興味がありそうな知り合いを巻き込みメンバーは3人に．初めは大学のラウンジ的なところで行うつもりでしたが，CAMPHOR-メンバー各位のご厚意により CAMPHOR- HOUSEで開催する運びとなりました．
勉強会
2015年9月に勢いで始まった勉強会でしたが，皆飽きることなく着実に回を重ね，半年間で14回の勉強会を行いました．SoftwareFoundations(日本語翻訳版）に沿ってスクリーンでスクリプトを読み込みながら，疑問点を話しあったり証明を考えたりという形で勉強会は進みました．
主なトピックを以下に一覧します．
- Coqの使い方・基礎
- 帰納法
- 論理と計算の関係性
- プログラミング言語の形式的定義及び議論
- コード生成（ @ymyzk 先生による臨時講義 ）
カリー・ハワード同型対応を利用したCoq自体の面白さを超えて，プログラミング言語の性質を示したり，Coqで性質が示されたコードを別の実用的な言語へと変換したりといった部分にも触れることができました．付け焼き刃の知識を流し込むのではなく，時間をかけてじっくりと地力を高める勉強会になったのではないかと思います．
最後に
CAMPHOR- HOUSEにはスクリーン・プロジェクター・ホワイトボード・各種飲み物など，勉強会に必要な備品が揃っています．今回のように少人数で定期的に開催する勉強会も大歓迎です．勉強したい技術・分野があるけど一人では続かなそう……と悩んだ時は，HOUSEやSlackで相談してみると一緒に勉強する人が集まるかもしれませんよ！