GitHub - pirapira/coq2rust: Coq to Rust program extraction. The whole tree is on the original Coq code base.You 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
homebrew で MathComp を入れる - amutake's blog
追記 2015/11/11 今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。 opam repo add coq-released https://coq.inria.fr/opam/released # opam に Coq 関連のライブラリを追加 opam install -j4 coq.8.4.6 coq:ssreflect.1.5.0 coq:math-comp.1.5.0 # 安定版を指定してのインストール MathComp (mathematical components) は Coq の拡張である SSReflect を使った、数学系の問題に特化したライブラリです。 で、Mac でよく使われているパッケージマネージャである homebrew には coq も ssreflect も標準であるのに、なぜか mathcomp
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
Coq/SSReflect/MathComp Tutorial
資料: 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
Verified Software Toolchain
Rationale In some application domains it is not enough to build reliable software systems, one wants proved-correct software. This is the case for safety-critical systems (where software bugs can cause injury or death) and for security-critical applications (where an attacker is deliberately searching for, and exploiting, software bugs). Since proofs are large and complex, the proof-checking must
ProofCafe - 名古屋を中心に活動する定理証明器・関数型言語のコミュニティ
開催勉強会 ProofCafeではいくつかの勉強会を定期開催しています。 詳細は個別のページをご覧ください。 Coqを用いたプログラムの証明について勉強する勉強会です。 コーヒーを飲みながら楽しく証明しましょう。 TAPL-nagoya Types and Programming Laungages(通称TAPL)の読書会です。 ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。 休日カフェタイム, KCTNagoya 圏論に関する勉強会です。 どえりゃあ Haskell Haskellに関する勉強会です。 サービス Software Foundations(和訳) Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧 に説明されています。 Cochin Coqの定理検索サー
NII Shonan Summer School on Coq
2014年8月25日から2014年8月29日にかけて開催された NII Shona Summer School on Coq に関連したつぶやきのまとめです。
Programs and Proofs
Mechanizing Mathematics with Dependent Types Lecture notes with exercises Ilya Sergey These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reason
Autosubst: Automation for de Bruijn syntax and substitution in Coq
POPLmark Benchmark Comparison The POPLmark is a benchmark to "measur[e] progress [...] in mechanizing the metatheory of programming languages". We have implemented part A of the challange problem, the preservation and progress of System F with subtyping, to compare Autosubst to manual implementations and other libraries. The following are all Coq implementations of part 1A and 2A we know of. Leroy
Alea: a library for reasoning on randomized algorithms in Coq Version 8
Alea: a library for reasoning on randomized algorithms in Coq Version 8Christine Paulin-Mohring with contributions by David Baelde and Pierre Courtieu PROVAL Team LRI, UMR 8623 Univ. Paris-Sud 11, CNRS & INRIA Saclay - Île-de-FranceMay 2013 1 Introduction This library forms a basis for reasoning on randomised algorithms in the proof assistant Coq [5]. The source files are available from the (auth
OpenSSL #ccsinjection Vulnerability
[English] 最終更新日: Mon, 16 Jun 2014 18:21:23 +0900 CCS Injection Vulnerability 概要 OpenSSLのChangeCipherSpecメッセージの処理に欠陥が発見されました。 この脆弱性を悪用された場合、暗号通信の情報が漏えいする可能性があります。 サーバとクライアントの両方に影響があり、迅速な対応が求められます。 攻撃方法には充分な再現性があり、標的型攻撃等に利用される可能性は非常に高いと考えます。 対策 各ベンダから更新がリリースされると思われるので、それをインストールすることで対策できます。 （随時更新） Ubuntu Debian FreeBSD CentOS Red Hat 5 Red Hat 6 Amazon Linux AMI 原因 OpenSSLのChangeCipherSpecメッセージの処理に発見
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Sets in Coq, Coq in Sets
GitHub - coq-concurrency/pluto: A web server written in Coq.
Cat_on_Coq/src/Monoid at master · mathink/Cat_on_Coq · GitHub
CoqStyle
Ackerman's function in Coq
Copatterns Programming Infinite Objects by Observations
Heq : a Coq library for Heterogeneous Equality
Chapter 7 Proof handling
Proof General: 11. Coq Proof General