20100310

開催情報

日時：3/9 19:00-21:00
場所：銀座ルノアール新宿３丁目ビッグスビル店 2号室
定員：5名でとったけど10名まではいけまっせー。
http://atnd.org/events/3421

アジェンダ

• 今回からは、Coq(とできればEvent-B)を、ツールを動かしながら勉強していきます。
• 範囲を命題論理の証明だけに限定して、Coqに慣れましょう。
• 各自 Coq の実行環境をインストールしてきて下さい。　インストール方法(http://www39.atwiki.jp/fm-forum/pages/16.html) 　MacOS (Snow Leopard)とかLinuxの人はインストール手順を　Wikiに反映していただけると嬉しいです。
• The Coq Proof Assistant, A Tutorial (http://www39.atwiki.jp/fm-forum/pages/17.html) のChapter 1.3まで(p.18 まで)を、予め実際に自分で入力してみてください。　CoqIDEとかにチュートリアルの内容を入力したらsaveすると入力した事が全部記録されます。それを上から順に一行づつステップ実行して、皆で交代で発表しましょう。
• 当日時間があればガリグ先生の教材(http://www.math.nagoya-u.ac.jp/~garrigue/lecture/ 2009_AW/coq2.pdf) の練習問題を解きます。
• 何か関連した面白い話を準備出来る人は歓迎。時間配分を考える必要があるので、予め立候補して頂けると嬉しいです。
• 会議室利用料金約6000円は割り勘です。

• OCaml-Javaを使って、CoqからJavaのコード生成までやってみる。

議事録

関連ページ

• Coq命題論理の証明