資料: 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
What is ProofWeb? ProofWeb is both a system for teaching logic and for using proof assistants through the web. ProofWeb can be used in three ways. First, one can use the guest login, for which one does not even need to register. Secondly, a user can be a student in a logic or proof assistants course. We are hosting courses free of charge. If you are a teacher and would like to host your course on
PeaCoq is a web-based front-end to the Coq proof assistant. It provides an interface similar to CoqIDE or ProofGeneral, but additionally offers a proof mode called "Proof Tree" with the following features: preview of the outcome of running a tactic visual diff of the context before and after a tactic context clutter reduction using browser overlay Publications Stay tuned... Source View on Github C
This is a proof market for Coq. The list of all problems Create a new problem Recent answers How to get proofs done for bitcoins Create a new problem wait for somebody to solve the problem on recent entries pay bitcoins see the proof How to get bitcoins for proving find a problem on the list of all problems (optional) contact possible payers solve the problem post your solution with a price and yo
autoのように高度な機能を持ったtacticを使用した時に、 何が起きたのかわかないということがよくあると思います。 そのようなときはtactic名の前にinfoをつけることで、 具体的にどのようなtacticが適用されたのかを見ることができます。
Coq'Art is the familiar name for the first book on the Coq proof assistant and its underlying theory the Calculus of Inductive Constructions , written by Yves Bertot and Pierre Cast�ran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Cast�ran, Pierre 2004, XXV, 469 p.,
Overview Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. (See the list of supported provers below.) Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, s
This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since s
Download Coq(英語) ダウンロードしなければ何も始まらない。 Download | The Coq Proof Assistant ちなみにLinuxディストリならcoqideパッケージをインストールするのが吉 Coqの入門記事を書く会 そこそこ体系的な入門サイト 2010-09-02 - ひとり勉強会 2010-09-14 - ひとり勉強会 2010-09-19 - ひとり勉強会 2010-10-12 - ひとり勉強会 Coq 99 練習問題。直観主義論理における有名な証明を一通り解ける。 Functional Programming Memo: [Coq] Coq-99 : Part 1 anarchy proof 練習用サイト。途中から一気に難化するのが問題。 わからなかったら他の人の解答も見られる anarchy proof - Curry-Howard Isomorp
eq_nat is recursively defined to test equality of two natural numbers n and m by pattern matching on their constructions. It returns true if both are 0, or if their successors S n' and S m' are recursively equal; otherwise it returns false. Evaluating eq_nat 3 3 returns true since 3 is constructed by applying S twice to 0, and both arguments have the same construction.Read less
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
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]。 懇
forall についての雑文 さて、ここで教科書の Coq in a Hurry に戻ると、私が作った「風が吹く」「桶屋が儲かる」なんかの命題を Variable で定義する代わりに、forall というキーワードを使っています。つまり、 Variable 風が吹く 桶屋が儲かる : Prop. Theorem 風桶 : (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる の代わりに Theorem 風桶 : forall 風が吹く 桶屋が儲かる:Prop, (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる. とやっても、だいたい同じように証明できるという事です(intro が二つ余分に必要です)。ではそもそも forall とは何でしょうか？ forall とは、universal quantifier (全称記号)といって、「すべての何とか」を表す
What is Proof General? Proof General is a generic interface for proof assistants (also known as interactive theorem provers), based on the extensible, customizable text editor Emacs. Proof General has been developed at the LFCS in the University of Edinburgh, mainly by David Aspinall, with contributions from other sites. It is distributed under the conditions of the GNU General Public License v3.0
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain f
雑多な文書 † Coq/install インストールのしかた(cygwin+Meadow) Coq/tactics tactic の中途半端な解説 Coq/Proofs? 証明したこと
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
