Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか？ プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？ プログラムを「証明する」ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE：Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ
なぜCoqが重要か
結論 最強のプログラム検証器 最強の関数型言語 最強のプログラム検証器 Coqは最強の表現力を持つ仕様記述言語を使う 仕様記述言語は検証したいこと を記述するための言語 表現力は検証器によって全然違う 表現できる範囲が、検証器の限界 Coqのそれは高階述語論理 ← 最強 最強のプログラム検証器 Coqを使うためにはPhDが必要? 高校生でも練習すればできる (c.f. プログラミングCoq) 最強のプログラム検証器 証明を人間が与えるのが大変？ タクティックによる自動化はOCamlでいくらでも可能 型チェッカはタクティックと独立なので安全 既にomegaなどの自動証明アルゴリズムを実装したタクティックあり 最強の関数型言語 Coqは(型の表現力が)最強の関数型言語 型の表現力が最強 型推論は完全ではない 停止性は保証しなければならない 注意: ここでの関数型言語とは (ラムダ計算を基礎とし
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
