タグ

coqに関するtyruのブックマーク (3)

  • プログラムに証明が付く日 | RANDMAX

    この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。 http://qiita.com/advent-calendar/2013/theorem_prover 神田「野らぼー」にて、地下の薄暗い店内で… 「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」 「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ!ってことになる。」 「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析っ

    プログラムに証明が付く日 | RANDMAX
    tyru
    tyru 2013/12/09
  • 『ソフトウェアの基礎』のePub版を公開しました。 - みずぴー日記

    「Software Foundations(和訳: ソフトウェアの基礎)」はBenjamin Pierce氏らによって書かれたドキュメントであり、Coqによりプログラミングやプログラミング言語の理論が解説されています。基的な部分から丁寧に解説されているため、Coqの入門書としてもプログラミング言語理論の入門書としても、非常に優れた内容となっています。 今回は、その「ソフトウェアの基礎」のePub版を公開しました。 対応したリーダを用いることで、iPhoneiPadAndroidドキュメントを読むことができます。 ダウンロード http://proofcafe.org/sf-beta/ からダウンロードできます。 またmobi版もありますが、Kindleを持ってないので、動作確認はしていません。 バグ報告 http://github.com/sfja/sfja へのissues登録

    『ソフトウェアの基礎』のePub版を公開しました。 - みずぴー日記
    tyru
    tyru 2012/07/16
  • IIJ Research Laboratory

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

  • 1