Untitled Document
3. Arithmetic omega - Presburger arithmetic (propositional formulas, with equalities, inequalities, for nat and Z) auto with arith - ring - associative commutative rewriting field - equalities in commutative fields (like ring, but with division) fourier - linear inequations with propositional structure, on real numbers 4. Induction Introduction (prove inductive facts) apply - treat each constructo
Coqの入門記事を書く会 (1) - ひとり勉強会
証明支援系Coqの遊び方の入門を書いてみるよ。すでに世の中に何個も入門記事ありますけど、増えて困ることはなかろう…ということで。まず、インストール方法については、id:yoshihiro503 による紹介記事 http://d.hatena.ne.jp/yoshihiro503/20070706#p1 最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。 を参照のこと。現時点では最新の安定版の Coq 8.2 がおすすめ。
Coqで依存型 - にわとり小屋でのプログラミング
最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。 Variable A:Set. Inductive Vec : nat -> Set := | VNil : Vec O | VCons : forall n, A -> Vec n -> Vec (S n). このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。 例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値
Gallina の構文と Vernacular コマンド
Gallina の構文と Vernacular コマンド 字句 空白文字、改行、タブは空白とみなされる。 コメントは (* で始まり *) で終わる。コメントの中に他のコメントあるいは文字列を入れることができる。コメントは空白とみなされる。 識別子には、英字 (A, B, …)、下線 (_) その他 Unicode で識別子として利用可能とされている文字が使える。識別子の二文字目以降には数字およびプライム (') も使える。 キーワード 特殊な意味を持つため識別子として使えないキーワードは以下の通り: _ as at cofix else end exists exists2 fix for forall fun if IF in let match mod Prop return Set then Type using where with 項 全称量化子 forall n, 0 fo
CoqUn2010
23. Record Mem := mkMem { nodes : set A; roots : set A; frees : set A; next : A -> option A; marker : A -> mark; }. 18 24. Record Mem := mkMem { nodes : set A;← roots : set A; frees : set A; next : A -> option A; marker : A -> mark; }. 18 25. Record Mem := mkMem { nodes : set A;← roots : set A;← frees : set A; next : A -> option A; marker : A -> mark; }. 18
Coq Tutorial
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
Coq参考資料 - fm-forum @ ウィキ
Coq参考資料 教科書 "Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive" Springerから出版されている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 Assi
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - mzp/GC: Proof of Garbage Collector
Proof General: 1. Introducing Proof General