GitHub - bacam/coqjvm: Coq executable semantics and resource verifierYou signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
Extensible core Featherweight Java
Core Featherweight Java (cFJ) is a variant of Featherweight Java without casts. This Coq development is meant to demonstrate how to design mechanized metatheory definitions and proofs in an extensible way. There are a number of different features that can be added to uFJ to build new variants of the language. These proofs were checked with Coq version version 8.3pl2. Earlier versions of Coq might
ProofSummit 2011 で『CoqによるMsgPackシリアライザの証明と実装』という話をしました。 - みずぴー日記
ProofSummit2011でMsgPackを証明したときの話をしてきました。内容は名古屋Reject会議で話したことを膨らませた感じになっています。 話の趣旨としては「バグって怖いじゃん → じゃあ証明しようぜ → やってみた」みたいな感じです。 スライド CoqによるMsgPackの証明 View more presentations from Hiroki Mizuno ustream http://www.ustream.tv/recorded/17493318 感想 新宿ダンジョンこわい [twitter:@ikegami__]さんと[twitter:@masahiro_sakai]さんにAgdaを教えてもらえたので、とてもよかった Software Foundationsの和訳プロジェクト、気になります
Proviola
The Proviola is a tool set for generating a dynamic (HTML + JavaScript) page out of a Coq proof script. The generated page can be used to display proof states without having the reader load the script into a proof assistant instance, giving a considerable advantage over browsing a repository of static files.The script below is a minimal example of a movie generated using the Proviola. Point to the
applpi
Applpi is a library in the Coq proof assistant that enables concurrent programs to be modeled and verified in Coq, and the models to be run as OCaml programs. It contains a formalization of a concurrent language based on the pi-calculus, a formalization of a specification language based on spatial logic and lemmas for formal verification. Applpi has been applied to the verification of an HTTP serv
Coqで分離論理(separation logic) - keigoiの日記
分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これは Aで言及しているポインタと、 Bで言及しているポインタが指しているヒープ領域が、分離されている(≒エイリアシングがない)ことをいっている。 Affeldtさんが、Coqで分離論理を書いて、しかもそれを公開してくださっている。 http://staff.aist.go.jp/reynald.affeldt/seplog/ C言語で書かれたOSのヒープマネージャや、SmartMIPSのアセンブラで書かれた暗号プリミティブの検証をCoqでやっている。 こういったことを自分でも触れるようになりたいので、ICFEM2006のソースを写経して
Formal Verification of Memory Properties
We are interested in the formal verification of low-level software. For this purpose, we have developed in the Coq proof assistant formalizations of Separation logic (as presented in the survey by John C. Reynolds). We have applied these formalizations to several use-cases, including: the verification of the heap manager of the Topsy operating system (paper) the verification of arithmetic function
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
CoqのSortについて
山本和彦 @kazu_yamamoto sort の訳語を募集します。 「型の型」ぐらいですか？ Haskell の kind と区別がつくことを希望。 #coqt 2011-02-28 10:13:49
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]。 懇
Coqで多重再帰のデータ構造を証明する - にわとり小屋でのプログラミング
Coqでは一重の再帰的なデータは例えば次の様に定義できる。 Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A). Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。 list_indは次の様な型を持っている。 Coq < Check list_ind. list_ind : forall (A : Set) (P : list A -> Prop), P (Nil A) -> (forall (x : A) (xs : list A), P xs -> P (Cons A x xs)) -> forall l : list A, P l このlist_indは帰納法に関して非常に強力である。 リストを引数に持つような任意の述語Pに対し
Formalizing 100 Theorems
Theorems in the list which have not been formalized yet are in italics. Formalizations of constructive proofs are in italics too. The difficult proofs in the list (according to John all the others are not a serious challenge "given a week or two") have been underlined. The formalizations under a theorem are in the order of the list of systems, and not in chronological order. The List The Irrationa
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
refineタクティックでらくらく依存型プログラミング(?) - keigoiの日記
下の記事では， Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}. という関数を，Coqの証明モードで作りました．ところが証明モードで作ったプログラムは極めて複雑でイマイチ効率のほどがよくわかりません (Coqで Print dual_dec. するとわかります)． ソートSetの部分だけを見ればdual_decは非常に簡単な関数で，dual_boolで見たように高々項の深さ回数*2のパターンマッチで書けるはずです． というわけで，dual_dec を 直接 λ項で書き下してみましょう．ただし，せっかくCoqを使うので，証明が必要な部分は極力 証明モードを使います． そういう用途には refineタクティックを使います．どうやって証明していいかわからない部分を _ にしておく
Coq Tips
以下、Parameters A B C P Q R : Prop. を仮定。 目次 前件 (仮定) が……の場合 仮定が False の場合・仮定に矛盾がある場合 仮定が否定の場合 (~A の形) 仮定が含意の場合 (A -> B の形) 仮定が連言の場合 (A /\ B の形) 仮定が選言の場合 (A \/ B の形) 仮定が全称量化子 (forall) の場合 仮定が存在量化子 (exists) の場合 後件 (ゴール) が……の場合 ゴールが True の場合 ゴールが False・否定の場合 ゴールが含意の場合 (A -> B の形) ゴールが連言の場合 (A /\ B の形) ゴールが選言の場合 (A \/ B の形) ゴールが全称量化子 (forall) の場合 ゴールが存在量化子 (exists) の場合 ゴールが恒真命題 (トートロジー)
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
https://dl.acm.org/citation.cfm?id=1786136
CiteSeerX
Separation Logic: A Logic for Shared Mutable Data Structures
Announcing Ssreflect 1.1 | The Coq Proof Assistant