20100310

※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

開催情報

日時:3/9 19:00-21:00
場所:銀座ルノアール新宿3丁目ビッグスビル店 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のコード生成までやってみる。

議事録


関連ページ

最終更新:2010年03月10日 00:02
ツールボックス

下から選んでください:

新しいページを作成する
ヘルプ / FAQ もご覧ください。