『ソフトウェアの基礎』のePub版を公開しました。 - みずぴー日記
「Software Foundations(和訳: ソフトウェアの基礎)」はBenjamin Pierce氏らによって書かれたドキュメントであり、Coqによりプログラミングやプログラミング言語の理論が解説されています。基本的な部分から丁寧に解説されているため、Coqの入門書としてもプログラミング言語理論の入門書としても、非常に優れた内容となっています。 今回は、その「ソフトウェアの基礎」のePub版を公開しました。 対応したリーダを用いることで、iPhoneやiPad、Androidで本ドキュメントを読むことができます。 ダウンロード http://proofcafe.org/sf-beta/ からダウンロードできます。 またmobi版もありますが、Kindleを持ってないので、動作確認はしていません。 バグ報告 http://github.com/sfja/sfja へのissues登録
OCamlコードをCoqで検証できる "CFML" で 証明コンペに挑戦 (未完) - keigoiの日記
VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るのは見送った（というかチームの人数上限4人で入れなかった）。 仕事や出張の片手間でやっていたので、結局一問も検証できなかったけど、楽しかった。 検証にはCFMLというツールを勉強しながら使った。 これを使えば OCaml のソースコードを Coq で検証できる。 それも ref型による破壊的代入つきの手続き的なOCamlを含む。 そして Coqと違い、プログラムは停止しなくてもいい。 つまり、CFMLを使えば、 手続き型プログラムを、ホーア論理+分離論理(のようなもの;後述)を使って
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
Coqでラムダ計算を証明してみた - みずぴー日記
前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機 let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式 型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT : type | FunT : type -> type -> type. 式は、変数参照、真偽値、ラムダ(関数抽象)、関数適用、if式。 Inductive term : Set := Var : string -> term | Bool : bool -> term | Lambda : string -> type -> term -> term | Apply : term -> term -> term | If : term -> term -> term -> term. 証明した定理 型
Coqのおかげで見つけれたバグ - みずぴー日記
最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。 で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直してみると、そもそもsubstitutionの定義が間違っていました。このバグはなかなか根が深くて、前に作ったトイ・コンパイラ(scalet)でも同じ間違いをしてました。 というわけで、これはCoqのおかげで見つけれたバグだし、人手は見付けづらいバグと言えないこともないので記録しておきます。 バグを含んだSubstitution まずはバグを含んだSubstitutionです。どこが間違っているか分かりますか? ボクは分かりませんでした。 (* subst *) Inductive Subst : term ->
ProofWeb
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
ポケットサーバー 格安レンタルサーバー
ポケットサーバー お探しのページが見つかりません。 貴方がアクセスしようとしたページは見つかりません。ページは削除されたか、アクセス先URLの間違いである場合が考えられます。 正しいURLをご確認ください。 このページの管理者の方で、予期せずこのページが表示されている場合は、事務局までお問い合わせください。 プチポケサーバーのページはこちら。 5秒後に自動的に移動します。
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Software Foundations 日本語版Wiki