タグ

関連タグで絞り込む (0)

  • 関連タグはありません

タグの絞り込みを解除

coqに関するarray08_12のブックマーク (5)

  • わかめモナ化.md

    わかめモナ化: Maybeモナドの証明 + Coq入門 証明の重要性 うかつにモナドと言うと刺される 例: jQueryはモナドだ - id:anatooのブログ 「jQueryはモナドである」と主張したけど、証明はなかったのですぐに刺された。 JQueryがモナドかどうかとか - たけをの日記@天竺から帰ってきたよ うーん… これ、いわゆる3つのモナド則じゃないよね。ココに書かれてるのはモナドの構造のこと、それもHaskellに特化したもので、圏論的な構造じゃない。抽象的に書けば、モナドは関手に2つの変換 unitjoin が付随したもの(Haskell の bind はこれらから導出できる)だし、更に 左単位則、右単位則、結合則の3つの法則を満たすたものでなければならない。 この記事で何をやりたかったかはわかるんだけど、でもうまく行ってないね。もし何かをモナドと呼ぶときはもっと厳

    わかめモナ化.md
  • ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation

    ソフトウェアの基礎(beta)¶ ドキュメントは実験中のものです。 安定板は http://proofcafe.org/sf/ を参照してください。 epub版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.epub mobi版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.mobi Contents:

  • IIJ Research Laboratory

    ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで

  • IIJ Research Laboratory

    ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで

  • Coqによる証明駆動開発

    わんくま同盟 名古屋勉強会 #16 http://www.wankuma.com/seminar/20110115nagoya16/Default.aspx で使う予定だったスライド。 証明駆動開発の簡単な紹介。じゃっかんTDDにケンカを売ってる:)

    Coqによる証明駆動開発
  • 1