fm-forum @ ウィキ

fm-forum @ ウィキ内検索 / 「Certified Programming with Dependent Types関係」で検索した結果

• Certified Programming with Dependent Types関係
  Certified Programming with Dependent Types (CPDT)を読む為の前提 この教科書は、オリジナルなtacticのcrushというのを導入して、色々自動証明をさせています。なので、crush出来る様にしておかないと、教科書の証明を写経できません。crushを使う方法ですが、 Coqをインストールしておくのは当然。 CPDTの付属ファイルを入手する。詳しくはCPDT 1.6章を読むべきだが http //adam.chlipala.net/cpdt/cpdt.tgz をダウンロードする。 適当なディレクトリ (~/cpdt/とか)で展開し、makeする。 Coq起動時に、coqtop -I ~/cpdt/src とオプションでソースディレクトリを指定。 Coq内で、Require Import Tactics. と Tactics.v ...
• トップページ
  ...資料Coq勉強資料 Certified Programming with Dependent Types Event-B勉強資料 Slides and Rodin Platform archives of the developments corresponding to chapters of the books Coq Coqインストール Coq参考資料 Certified Programming with Dependent Types関係 Coq命題論理の証明 Coqで数独 SPIN SPINインストール リンク集：関連しそうな話へのリンク集
• Coq参考資料
  ...だが値段も高い。 Certified Programming with Dependent Types (http //adam.chlipala.net/cpdt/) Harvardの授業で使用 (PDF 360ページ程度)。定期的に改訂されている。 (Latest 2010/2/3) CPDTは関数型言語プログラマにとってCoqを理解しやすいいいテキストだと思います。 読む時は「Certified Programming with Dependent Types関係」も参照の事。 チュートリアル The Coq Proof Assistant, A Tutorial (http //coq.inria.fr/V8.1/files/doc/Tutorial.pdf) Coqを使って簡単な証明をするサンプル多め。(44 pages) 日本語によるTutorial解説。最初の...
• 書籍
  和書 形式手法の技術講座 (佐原伸/SRC) VDM++ プログラム仕様記述論 (荒木啓次郎/オーム社) VDM-SL, Z ソフトウェア科学基礎 Bメソッドによる形式仕様記述 SPINモデル検査―検証モデリング技法 (中島震/近代科学社) SPIN 形式手法モデル理論アプローチ (高原康彦 他/日科技連) MTA-SDK ディペンダブルシステム SPINによる設計モデル検証 (吉岡信和 他/近代科学社 TopSE) SPIN 4日で学ぶモデル検査 (初級編) (産業技術総合研究所システム検証センター/NTS) NuSMV, SPIN; KNOPPIX CD-ROM付 組み込みソフトウェアの設計 検証 ソフトウェア開発のモデル化技法 (J.フォッツジェラルド/P.G.ラーセン/岩波) VDM-SL 組み込みソフトウェア2007 モデルに基づく開発方法論の全て (日経BP) 日経エレクト...
• イベント
  形式手法に関係したセミナー、勉強会、学会などありましたらどんどん追加してください。 イベント参加結果はぜひ、ご報告ください。 2010/8/29 Coq庵@名古屋 2010/8/23-30 2nd Asian-Pacific Summer School on Formal Methods@北京 2010/8/9-10 第二回層圏トポス合宿(8月9日-10日)@代々木オリンピックセンター 2010/7/11-14 ITP2010(Interactive Theorem Proving) 2010/7/12 13 00-17 00 Alloyセミナー@名古屋 2010/6/9-11 ソフトウェア・シンポジウム 2010 横浜 2010/5/12 形式手法徹底解説@ESEC 2010/4/29 第4回Formal Methods 勉強会 2010/4/25 Proof Cafe(栄) ...
• プラグイン/ニュース
  ニュース @wikiのwikiモードでは #news(興味のある単語) と入力することで、あるキーワードに関連するニュース一覧を表示することができます 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_174_ja.html たとえば、#news(wiki)と入力すると以下のように表示されます。 【グランサガ】リセマラ当たりランキング - グランサガ攻略wiki - Gamerch(ゲーマチ) 【まおりゅう】八星之紋章交換のおすすめ交換キャラ - AppMedia(アップメディア) Among Us攻略Wiki【アマングアス・アモングアス】 - Gamerch(ゲーマチ) マニュアル作成に便利な「画像編集」機能を提供開始！ - ナレッジ共有・社内wikiツール「NotePM」：時事ドットコム - 時事通信 マニ...
• 開催記録
  2010/2/8 第1会Formal Methods 勉強会 http //atnd.org/events/2968 Agendaトップエスイーチュートリアルセミナー「Bメソッドによる形式仕様記述」復習(小林健一) UMLからAlloyへ(小林健一) Coq and Why Formal Verification Tools(tmiya) http //homepage.mac.com/takashi_miyamoto/coq/Coq_20100208a.pdf http //www.slideshare.net/tmiya/coq-20100208a 勉強会名前決定 今後の進め方 今後の進め方Coqの勉強(http //adam.chlipala.net/cpdt/) B-Methodsの勉強(http //wiki.event-b.org/index.php/Event-B_Lang...
• 20100208
  2010/2/8 第1会Formal Methods 勉強会 http //atnd.org/events/2968 Agendaトップエスイーチュートリアルセミナー「Bメソッドによる形式仕様記述」復習(小林健一) UMLからAlloyへ(小林健一) Coq and Why Formal Verification Tools(tmiya) http //homepage.mac.com/takashi_miyamoto/coq/Coq_20100208a.pdf http //www.slideshare.net/tmiya/coq-20100208a 勉強会名前決定 今後の進め方 今後の進め方Coqの勉強(http //adam.chlipala.net/cpdt/) B-Methodsの勉強(http //wiki.event-b.org/index.php/Event-B_Lang...
• 第1回(2010/2/8)
  2010/2/8 第1会Formal Methods 勉強会 http //atnd.org/events/2968 Agendaトップエスイーチュートリアルセミナー「Bメソッドによる形式仕様記述」復習(小林健一) UMLからAlloyへ(小林健一) Coq and Why Formal Verification Tools(tmiya) http //homepage.mac.com/takashi_miyamoto/coq/Coq_20100208a.pdf http //www.slideshare.net/tmiya/coq-20100208a 勉強会名前決定 今後の進め方 今後の進め方Coqの勉強(http //adam.chlipala.net/cpdt/) B-Methodsの勉強(http //wiki.event-b.org/index.php/Event-B_Lang...
• Coqインストール
  Coqインストール Coqダウンロード先ページ Linuxの場合 Ubuntu または Debian の場合 # sudo apt-get install coq coqide ソースから最新版をインストールする場合 ソースからインストールするためにはocaml, camlp5が必要です。ソースにはREADMEの他にINSTALLというファイルがあって、そこにインストールするための詳細が記述されています。 OCamlがなければインストール (see http //ocaml.jp/インストール方法) camlp5のインストール (http //pauillac.inria.fr/~ddr/camlp5/からcamlp5-XXX.tgz をダウンロードする) $ ./configure --transitional $ make world.opt $ make ins...
• プラグイン/人気商品一覧
  人気商品一覧 @wikiのwikiモードでは #price_list(カテゴリ名) と入力することで、あるカテゴリの売れ筋商品のリストを表示することができます。 カテゴリには以下のキーワードがご利用できます。 キーワード 表示される内容 ps3 PlayStation3 ps2 PlayStation3 psp PSP wii Wii xbox XBOX nds Nintendo DS desctop-pc デスクトップパソコン note-pc ノートパソコン mp3player デジタルオーディオプレイヤー kaden 家電 aircon エアコン camera カメラ game-toy ゲーム・おもちゃ全般 all 指定無し 空白の場合はランダムな商品が表示されます。 ※このプラグインは価格比較サイト@PRICEのデータを利用しています。 ...
• メニュー
  メニュー トップページ 勉強会 イベント 書籍 リンク 情報交換手段 メーリングリスト twitter @fm_forum_ ustream Skype 各形式手法資料 Alloy B-Method Coq Event-B ここを編集
• 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/...
• 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.j...
• Coq命題論理の証明
  Coq命題論理の証明 命題論理の例題をtautoに頼らずに証明するためのTips 大まかなtacticを使う順序 大体、下記の原則で考える。 まずgoalをintroを使って分解して、goalを簡単にし、仮定を増やす事を考える。 goalが - の式の場合（演算子順序を考えると A - B の形の式と考えられる場合）は、intro, intros などを使えばOK、 goalが ~ の式（演算子順序を考えると ~X の形）の場合、goalがFalseになるまでintroして、「goal=Falseの場合」へ。 goalを導ける仮定がある場合（goalがAで、H X- A のような仮定がある場合）、apply H してgoalをXに変更する。 goal, 仮定の /¥, ¥/ は基本的には仮定の方から先に処理するのが楽だと思う。 仮定が H A /¥ B の形...
• @wiki全体から「Certified Programming with Dependent Types関係」で調べる

更新順にページ一覧表示 | 作成順にページ一覧表示 | ページ名順にページ一覧表示 | wiki内検索