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をやりましょう。


議事録

タグ:

+ タグ編集
  • タグ:

このサイトはreCAPTCHAによって保護されており、Googleの プライバシーポリシー利用規約 が適用されます。

最終更新:2010年04月03日 23:12
ツールボックス

下から選んでください:

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