partake.inThis domain may be for sale!
NII Shonan Summer School on Coq
2014年8月25日から2014年8月29日にかけて開催された NII Shona Summer School on Coq に関連したつぶやきのまとめです。
Coq: Vernacular コマンド備忘録 - Qiita
のという式が使えるようになる。この andb 3 true は、実際には andb (nat_to_bool 3) true として処理される。 coercion には型強制という訳が充てられているみたいだけど、 Coq の場合、 implicit に変換函数を適用してみるという感じなので、 強制 ってほどでもないなぁと思わなくもない。 Set Printing Coercions. 変換函数の暗黙の適用は、基本的に Coq の出力上には現れない。 コードに書かれていないのだから、表示もされてない方が自然だ。 ただまぁ、変換函数についての性質を使うときとか、やっぱり変換函数が見えていたほうが良い時もある。 そんなときは事前に Set Printing Coercions. を実行しておくと良い。 解除は Unset Printing Coercions. で。 coercion を多用して
#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
|2^N|>|N| - くるるの数学ノート
まあすでにやっている人は多いと思いますが、昨日突然思いついて、自然数の集合が非可算個あることをCoqで証明してみました。 Require Import Arith. Definition diag (F : nat -> (nat -> bool)) (n : nat) : bool := negb (F n n). Theorem nat_to_nat_uncountable : forall (F : nat -> (nat -> bool)), exists (g : nat -> bool), forall (n : nat), F n <> g. Proof. intro F. exists (diag F). intro n. intro H. absurd (F n n = diag F n). unfold diag. intro H1. destruct (F n n).
Vim で Coq 環境を整える - 反省はしても後悔はしない
はじめに 昨日、スタート Ssreflect というイベントに参加して、Coq + ssreflect のハンズオン的なものをやりました。 Coq 環境といえば、Emacs の ProofGeneral が非常に有名です。 しかし、私は Emacs は終了の仕方すら分からないレベルの初心者なので Emacs + ProofGeneral ではチュートリアルの例題を打ち込むだけでも非常に苦労しました。 証明も普段使い慣れている Vim で何とかできないかと思い調べたところ、そこそこ良さ気な環境を構築できたので紹介します。 使用するプラグイン 以下の2つをインストールします。NeoBundle のようなパッケージマネージャを使用するのをおすすめします。 jvoorhis/coq.vim vim-scripts/CoqIDE jvoorhis/coq.vim は Coq のシンタックスとインデン
推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─ - λx. x K S K ＠はてな
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です． 元々このネタは， 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです． このため，ここで紹介するプログラムや証明は， タクティクの種類やライブラリの利用が必要最低限に絞られているので， もしかしたら Coq 初心者の方にも参考になるかもしれません (各タクティクの作用を明確に理解してもらうため，敢えて auto も使いませんでした)． Coq 上級者には冗長な証明が気になるかもしれませんが，その点は予めご了承ください． はじめに 比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ， クイックソートやマージソートをはじめとする多くの整列アルゴリズムがこれに属します (逆に比較ソー
プログラムに証明が付く日 | RANDMAX
この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。 http://qiita.com/advent-calendar/2013/theorem_prover 神田「野らぼー」にて、地下の薄暗い店内で… 「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」 「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ！ってことになる。」 「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析っ
ProofCafe - 名古屋を中心に活動する定理証明器・関数型言語のコミュニティ
開催勉強会 ProofCafeではいくつかの勉強会を定期開催しています。 詳細は個別のページをご覧ください。 Coqを用いたプログラムの証明について勉強する勉強会です。 コーヒーを飲みながら楽しく証明しましょう。 TAPL-nagoya Types and Programming Laungages(通称TAPL)の読書会です。 ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。 休日カフェタイム, KCTNagoya 圏論に関する勉強会です。 どえりゃあ Haskell Haskellに関する勉強会です。 サービス Software Foundations(和訳) Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧 に説明されています。 Cochin Coqの定理検索サー
VSTTE Competition参加記録 - みずぴー日記
id:yoshihiro503さんに誘われて、VSTTE Competitionというソフトウェア検証コンテストに参加しました。 「検証ツールに特に制限はないぜ」と書かれていたのでCoqを使いました。 競技プログラミンングに初めて参加しましたが、48時間ぶっとうしで同じ課題に取り組むのはとてもエキサイティングで楽しかったです。 参加メンバー [twitter:@yoshihiro503]さん [twitter:@pirapira]さん [twitter:@hirose_golf]さん ボク([twitter:@mzp]) 一日目 開始直前 yoshihiro503さんから"uiro,tebasaki,miso,..."と列挙された謎のメールが届く。 どうやらチーム名の候補だったらしいです。 yoshihiro503さんとSkypeで話しながらbitbucketの準備をしたりする。 0:00
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Yoshihiro503 on Twitter: "@mzp ocamlを入れる→camlp5-6.08を入れる→coqをソースからインストールする、でもいけました。 #raspberrypi #coq"
Yoshihiro503 on Twitter: "@suharahiromichi @morita_hm 私もssreflect-1.4を新しい環境にインストールしました。 ocaml-4.01.0 (from source) camlp5-6.11 (from source) coq-8.4pl2 (from source)"
Yoshihiro503 on Twitter: "coq-8.4はocaml-4.00.0 とcamlp5-6.06がある環境で、ソースからインストールできる。 #有益なことをつぶやこう #coq #ocaml #camlp5"
【魚拓】ProofTea(ProofCafe特別版) - PARTAKE
トップエスイーチュートリアル「Coqで学ぶ定理証明入門」
Sosuke MORIGUCHI on Twitter: "@yoshihiro503 Declare Moduleというコマンドですかね（そこまで使ったことがなかったので）"
partake.in
OpenSSLの新たな脆弱性 CCS Injection が発見される
partake.in
Coq.io
