Content-Length: 285874 | pFad | http://b.hatena.ne.jp/ruicc/coq/
Coq/SSReflect/MathComp Tutorial
資料: slides (last version): slides addendum about groups: html, pdf (automatically generated) slides (previous versions): [2015-07-24 Fri]: 京都大学の集中講義で使った資料(約14時間): slides (addendum about groups) [2014-12-15 Mon]: 名古屋大学の集中講義 で使った資料(約9時間): slides (addendum about groups) [2014-09-07 Sun]: 日本ソフトウェア科学会 第31回大会のチュートリアル (定理証明支援系Coq入門) で使った資料(4時間): slides Coq/SSReflect/MathCompの設定 参考文献: ssr.bib, coq.bib, it
Programs and Proofs
Mechanizing Mathematics with Dependent Types Lecture notes with exercises Ilya Sergey These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reason
Calculus of Construction on Web
Calculus of Construction on Web ヘルプ Powered by CoqInCoq, js_of_ocaml, and Coq
An Essence of SSReflect Iain Whiteside, David Aspinall, and Gudmund Grov CISA, School of Informatics University of Edinburgh Edinburgh EH8 9AB, Scotland Abstract. SSReflect is a powerful language for proving theorems in the Coq system. It has been used
An Essence of SSReflect Iain Whiteside, David Aspinall, and Gudmund Grov CISA, School of Informatics University of Edinburgh Edinburgh EH8 9AB, Scotland Abstract. SSReflect is a powerful language for proving theorems in the Coq system. It has been used for some of the largest proofs in formal mathematics thus far. However, although it constructs proofs in a formal system, like most other proof lang
2010年度後期・数理解析・計算機数学 III
[ ホーム | 講義 ] 2010年度後期・数理解析・計算機数学 III (同 概論III) レポート課題 プログラミング課題 提出期限 2010年12月 27日(月) レポート課題 提出期限 2010年2月7日(月) (M2は1月28日(金)) 講義予定 シラバス 第1回 10月6日 (10人) Objective Camlプログラミングの基礎: 定義と型 講義メモ 資料 EmacsでOCamlを使う (修正版) 第2回 10月13日 (7人) 多相型と汎関数 第3回 10月20日 (6人) 関数の証明と再帰関数 第4回 10月27日 (3人) 関数グラフの描画 関数描画ライブラリー plot.ml plot.mli リストと構造的帰納法 第5回 11月10日 (3人) 再帰的アルゴリズム1：リストと整列 講義メモ 第6回 11月17日 (3人) 再帰的アルゴリズム2：木構造と数式処理
CoqPratyで『CoqからRubyへ』という発表をしてきた - みずぴー日記
CoqPartyに参加してきました。すっげー楽しかった。 発表したこと From Coq to Ruby / CoqからRubyへView more presentations from mzpi. CoqのRuby Extractionを書いたときの話をしてきました。 Extractionを書けば、どの勉強会にもCoqの話で乗り込めるよ! 内容がid:yoshihiro503さんとかぶってたので、生成されたコードの解説をメインでしてました。 感想 Macのディスプレイアダプタをまた失くしたorz。 Coqの話がいっぱい聞けてたのしかったです。 [twitter:@maeda_]の「あなたの好きなtacticsは？」がステキすぎる。派生してあなぷるで人気のtacticsとかができたりした。 Redmine/Backlogにイカ娘を表示させるのは常識 by [twitter:@otf]。 懇
『ソフトウェアの基礎』のePub版を公開しました。 - みずぴー日記
「Software Foundations(和訳: ソフトウェアの基礎)」はBenjamin Pierce氏らによって書かれたドキュメントであり、Coqによりプログラミングやプログラミング言語の理論が解説されています。基本的な部分から丁寧に解説されているため、Coqの入門書としてもプログラミング言語理論の入門書としても、非常に優れた内容となっています。 今回は、その「ソフトウェアの基礎」のePub版を公開しました。 対応したリーダを用いることで、iPhoneやiPad、Androidで本ドキュメントを読むことができます。 ダウンロード http://proofcafe.org/sf-beta/ からダウンロードできます。 またmobi版もありますが、Kindleを持ってないので、動作確認はしていません。 バグ報告 http://github.com/sfja/sfja へのissues登録
fm-forum @ ウィキ
Formal Methods Forum 形式手法について広く深く研究する会です。 勉強会 参考資料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インストール リンク集：関連しそうな話へのリンク集
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Fetched URL: http://b.hatena.ne.jp/ruicc/coq/
Alternative Proxies:
セキュリティ診断・検査のGMOサイバーセキュリティ byイエラエ
ProofCafe - Front Page
ソフトウェアの基礎
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation
ProofCafe - Coq2Scala
名古屋Ruby会議で「Coq to Rubyで初める証明駆動開発」というタイトルで発表してきました - みずぴー日記
バグの無いプログラムを作ることは可能ですか？…