IIJ Research Laboratory

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

[pi8027]

読みましょう読みましょう

[t-wada]

うおおキタコレ! しかも書いているのは噂の女子大生の方か。続きが楽しみすぎます。

[sirocco]

「私はこの春から女子大生になります」って、凄い！ 理解しているだけでなく、この説明の能力は・・・どんな人なんだろう。一つ目の証明までは写経しながら読んだ。次二つ目の証明。#coqt

[antipop]

リアル数学ガ〜ルさんですか！

[areph]

認証駆動開発に興味があるので。

[tyoro1210]

女子大生と聞いて

[syque]

証明駆動開発やら P 言語 Coq やら。

[TRON]

こういう新機軸がドンドン出てくるから技術者はやめらんねぇなｗ

[risouf]

僕の周囲にも、こういうものがあるんだよってのが広まるといいなあ。 / ここで言う「絶対にバグのない」の意味を正しく理解できない人には（Coqを使いこなすことは）難しい。

[kjirouu]

コック

[itouhiro]

「プログラムの正しさを保証する用途。数学の定理証明にも（4色問題の場合分け、検証を手作業でなく機械的に証明）。CoqIDE、コンソールで対話的証明coqtop、Emacs。」

[lotz84]

読む

[gomi_ningen]

たのしそう

[iR3]

証明駆動開発 ですかぁ

[teematsu]

定理 証明

[stealthinu]

証明系言語Coqのチュートリアル。筆者の方、名前といい設定といいラノベっすか？とつっこみたくなるんですがこれはほんとなんだろうか…　HaskellもOCamlもやってねえよ… orz

[morita_non]

基本的に手順しか載ってなくて、あんまり分かりやすくなかった。高校生くらいで、証明だとか論理学だとか全般を直感的に理解出来る人向き。

[kiyo_hiko]

勉強

[masaru_b_cl]

いつかCoqをやるときのために

[heignamerican]

OCaml と Haskell どっちをやるべきか・・・

[sidestepism]

やってみてる

[musicala]

Coqを始めるなら、こっちのほうが馴染みやすそ。

[richard_raw]

定理証明支援系言語……ですか。しかも書いてたの女子大生ですか！

[murashit]

連載完結してた

[clouds-across-the-moon]

分かりやすい。丁寧。すばらしい

[Kureduki_Maari]

プログラミング Coq

[usamyu56]

メモ

[koki-h]

証明を使うことによって絶対バグがないプログラムが書けると。よく分からんが一応。

[noize_hioki]

テストが終わったら読む

[hengsu]

この春から女子大生なのにこの連載か

[cubeon]

サブタイトルは釣りです…と思うけどどうなんだろう…

[hiroqli]

Coq気になる

[taki0313]

読み物．おもしろい

[aaa131]

プログラミング

[heitatta]

遅ればせながら、Coqことはじめ。

[craccho]

初めて触れてみたけど面白い。ていうかこのブクマ数、こんなにメジャーな言語だったのか。ideでCtrl+hが使えないのがちょっとあれだった。

[cauchy_6]

読んだ

[picatiue]

〜 絶対にバグのないプログラムの書き方 〜