タグ

Coqに関するt_43zのブックマーク (4)

  • ニコニコをCoqで証明してみた / Yosh さん - ニコナレ

    2018年09月02日 10:042,24106ニコニコをCoqで証明してみた▲説明文を閉じるスライド制作者Yoshさんブログに貼り付け以下をコピーしてブログに貼り付けてくださいアカウントをお持ちの方ログインアカウントをお持ちでない方新規アカウント作成Now loading...エンコードが完了しました リロードしてください - / -コメントするコメント投稿するためにはログインしてくださいコメントリストページ一覧コメントページ123456789101112131415161718192021222324関連ナレッジニコニコ動画はなぜオワコン化しているのか ~…シリウスY さんねるねるねるねを練ったわけrerofumi さんデータでみるニコニコ動画の現状 -2018年5月myrmecoleon さん急上昇ナレッジninaさんの「【練習用】自分の声が、どんな声か…nina さんドワンゴプログ

    ニコニコをCoqで証明してみた / Yosh さん - ニコナレ
  • Coqで学ぶ証明プログラミング! テストだけでなく「証明」で安全性を保証する - エンジニアHub|Webエンジニアのキャリアを考える!

    Coqで学ぶ証明プログラミング! テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう! coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか? プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう! Coqって何? プログラムを「証明する」ってどういうこと? Coqを使ってみよう Coqのインストール方法 CoqIDE:Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ

    Coqで学ぶ証明プログラミング! テストだけでなく「証明」で安全性を保証する - エンジニアHub|Webエンジニアのキャリアを考える!
    t_43z
    t_43z 2018/08/20
  • ソフトウェアの基礎

    Benjamin C. Pierce Chris Casinghino Michael Greenberg Vilhelm Sjöberg Brent Yorgey with Andrew W. Appel, Arthur Chargueraud, Anthony Cowley, Jeffrey Foster, Michael Hicks, Ranjit Jhala, Greg Morrisett, Chung-chieh Shan, Leonid Spesivtsev, and Andrew Tolmach

    t_43z
    t_43z 2013/09/10
  • IIJ Research Laboratory

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

  • 1