20100410

開催情報

日時：4/10 13:00-19:00
場所：銀銀座ルノアールニュー大久保店 3号室 （東京都新宿区百人町1-18-8）
定員：10名でとったけど12名まではOK。
http://atnd.org/events/3687

アジェンダ

最終目標は形式手法を活用して仕事ができるようにすること！ まずは、考え方とツールに慣れるところから始めます。
初めての人にも導入資料へのリンクをお教えしますので、 レベル感を気にせず参加してください。

ただし、キャンセルは4/6 24:00までにお願いします （会議室料金は参加者で割り勘なので）。

• 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 まで)で、今回は1.4 Predicate Calculusの予定です。時間的に余裕があれば、予め実際に自分で入力（PDFからCoqIDEにコピペ）してみてください。入力したらsaveすると入力した事が全部記録されます。それを上から順に一行づつステップ実行して、皆で交代で発表しましょう。
  • 前回はガリグ先生の教材(http://www.math.nagoya-u.ac.jp/~garrigue/lecture/ 2009_AW/coq2.pdf) の練習問題を解きました。今回はガリグ先生の授業 (http://www.math.nagoya-u.ac.jp/~garrigue/lecture/2009_AW/coq3.pdf) の練習問題1.1を解こうと思ってます。
  • そこまで終わったら、CPDT (http://adam.chlipala.net/cpdt/) のChapter 3をやりましょう。

• Alloyの題材：
  • 現在検討中。 http://groups.google.co.jp/group/fm-forum に詳細を載せます。

議事録