Proof Market
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
Coqで独習するならどのページがいい？と聞かれたときのメモ - 簡潔なQ
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
Reverse Mathematics in Coq
This is a Korea-France research project on reverse mathematics. It is part of the STAR Project sponsored by the National Research Foundation on the Korean side and Ministry of Foreign and European Affairs on the French side. Besides two leaders of the project, Gyesik Lee on the Korean side and Hugo Herbelin on the French side, more researchers are involved, above all Laurent Bienvenu, Sungwoo Park
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Essential Incompleteness of Arithmetic Verified by Coq
Abstract A constructive proof of the Gödel-Rosser incompleteness theorem has been completed using the Coq proof assistant. Some theory of classical first-order logic over an arbitrary language is formalized. A development of primitive recursive functions is given, and all primitive recursive functions are proved to be representable in a weak axiom system. Formulas and proofs are encoded as natural
Welcome! | The Coq Proof Assistant
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
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
anarchy proof -
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20060427