Tsukuba Coq Users' Group
茨城県つくば市周辺の Coq ユーザのグループです。同人誌の発行等の活動をしています。 本 Coq による定理証明 2016.12 Coq による定理証明 2015.12 Coq による定理証明 2014.12 Coq による定理証明 2014.8 Coq による定理証明 2013.12 Coq による定理証明 - コンビネータ論理 C83版 Coq による定理証明 - Coq でスタック指向プログラミング 参加イベント コミックマーケット92 技術書典2 コミックマーケット91 コミックマーケット89 コミックマーケット87 コミックマーケット86 コミックマーケット85 メンバー 坂口 和彦 平井 洋一 石井 大海
COMIC ZIN 通信販売/商品詳細 Coq による定理証明 - Coq でスタック指向プログラミング
注目キーワード コミケ101NEW!! コミケ100 コミケ99 コミティア138 コミティア137 ・・・・・・・・・・・・・・・・・・・ うまぴょいNEW!! レトロゲームNEW!! 聖地巡礼NEW!! 旅行NEW!! 百合（同人）NEW!! ガルパン（同人）NEW!! 飲食系NEW!! TRPGNEW!! 評論NEW!! とびものNEW!! 鉄道 技術系NEW!! すごーい！ △NEW!! 響け！NEW!! 自転車NEW!! 若おかみ（JS）NEW!! FGO アイカツ！ ミリタリー 宇宙戦艦ヤマト ラブライブ！ 同人グッズNEW!! 艦隊これくしょん（同人）NEW!! ・・・・・・・・・・・・・・・・・・・ COMIC ZIN 専売NEW!! 商業誌 オリジナルNEW!! ニンジャスレイヤー アイドルマスター シンデレラガールズ THE iDOL M@STER 進撃の巨人 境界線上
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
Coqで独習するならどのページがいい？と聞かれたときのメモ - 簡潔なQ
Download Coq(英語) ダウンロードしなければ何も始まらない。 Download | The Coq Proof Assistant ちなみにLinuxディストリならcoqideパッケージをインストールするのが吉 Coqの入門記事を書く会 そこそこ体系的な入門サイト 2010-09-02 - ひとり勉強会 2010-09-14 - ひとり勉強会 2010-09-19 - ひとり勉強会 2010-10-12 - ひとり勉強会 Coq 99 練習問題。直観主義論理における有名な証明を一通り解ける。 Functional Programming Memo: [Coq] Coq-99 : Part 1 anarchy proof 練習用サイト。途中から一気に難化するのが問題。 わからなかったら他の人の解答も見られる anarchy proof - Curry-Howard Isomorp
にわとり小屋でのプログラミング日記
この記事はTppMark11の問題をCoqでやってみたという内容である。 問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義 変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>
プログラムに証明が付く日 | RANDMAX
この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。 http://qiita.com/advent-calendar/2013/theorem_prover 神田「野らぼー」にて、地下の薄暗い店内で… 「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」 「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ！ってことになる。」 「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析っ
Private Presentation
Private content!This content has been marked as private by the uploader.
目次一覧
■ 目次一覧 ホーム > 目次一覧 ■ 第1章 プログラムの正しさ —プログラムの検証入門— プログラムの正しさ プログラムの正当性とその証明法 —帰納的表明法— 検証条件 プログラムの停止性 演習問題 ■ 第2章 Floyd-Hoare 論理 Floyd-Hoare 論理 配列要素への代入文 演習問題 ■ 第3章 仕様としての事前条件と事後条件 配列の整列プログラム 配列を用いるプログラムの部分的正当性の例 仕様記述の例 演習問題 ■ 第4章 VDM-SL による仕様記述の例 簡単な仕様記述の例 有用な基本データ型 演習問題 ■ 第5章 例題で見るシステム仕様記述 住所録システム 参加登録システム 演習問題 ■ 第6章 事例で見る実用的仕様記述 対象とする自動販売機 自動販売機の抽象モデル モデルの拡張 ： ランプの導入 具体化 ： ボタンとカラムの導入 演習問題 ■ 付録A VDM-S
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
プログラム仕様記述論