Coqチュートリアル: @zakky_devさんが証明をできるようになるまで - みずぴー日記
先日、東京の会社から名古屋の会社に転職された@zakky_devさんの歓迎会がありました*1 。そこで、@zakky_devさんにCoqでリストの結合則を証明するチュートリアルをやってもらいました。 せっかくなので、そのときの台本を公開します。だいたい30分くらいの内容です。 Coqのインストール ぐぐりましょう。 Welcome ! | The Coq Proof Assistant Coq を始めよう Coqとは みなさん、自動化してる・してないなどの違いはあると思うんですが、プログラムを書いたらテストをすると思います。 ただテストはどうしても「こういう入力があったら、こういう出力がある」というのを並べていくことになるので、どうしても有限のパターンしか確認できません。 で、これで十分なこともあるんですが、中にはものすごい信頼性がいるプログラムで、有限のパターンの保証だけではたりない場合
わかめモナ化.md
わかめモナ化: Maybeモナドの証明 + Coq入門 証明の重要性 うかつにモナドと言うと刺される 例: jQueryはモナドだ - id:anatooのブログ 「jQueryはモナドである」と主張したけど、証明はなかったのですぐに刺された。 JQueryがモナドかどうかとか - たけをの日記＠天竺から帰ってきたよ うーん… これ、いわゆる3つのモナド則じゃないよね。ココに書かれてるのはモナドの構造のこと、それもHaskellに特化したもので、圏論的な構造じゃない。抽象的に書けば、モナドは関手に2つの変換 unit と join が付随したもの（Haskell の bind はこれらから導出できる）だし、更に 左単位則、右単位則、結合則の3つの法則を満たすたものでなければならない。 この記事で何をやりたかったかはわかるんだけど、でもうまく行ってないね。もし何かをモナドと呼ぶときはもっと厳
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
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のソースを写経して
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
セキュリティ診断・検査のGMOサイバーセキュリティ byイエラエ
定理証明支援系Coq を用いたプログラム運算