関数型言語でプログラミングできない人が読む「プログラミング Coq」 - risou style
なにやら日本語で書かれた定理証明支援系言語 Coq の良質なチュートリアルが公開されたとのことで、とりあえず読んでみました。 http://www.iij-ii.co.jp/lab/techdoc/coqt/ 定理証明支援系とは何か、 Coq で何ができるのか、という話題についてはここでは触れませんので、興味のある方は検索してみるなり、 Twitter でハッシュタグ #coqt をつけて誰かに聞いてみるのが良いと思います。 さて、公開された最初の記事「http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html」では最初に読者に前提として求める知識についての記述があります。 読者の前提知識としては OCaml や Haskell などの関数型言語でプログラミングできることを想定します。 http://www.iij-ii.co.jp/lab/te
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Welcome! | The Coq Proof Assistant
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain f
Coq - PukiWiki
Coq † http://coq.inria.fr/ Coq は、INRIA にて開発されている対話的定理証明支援系です。 Calculus of Inductive Construction (CIC) を基礎とし、Tactics と呼ばれるコマンドを駆使することにより証明を行います。 ↑ メモ † インストールする Coq 本体 Proofgeneral 証明をやってみる 簡単なものから Tactics リスト 証明の裏で何が起こっているのか 証明の実例 理論的 background Dependently Typed Lambda Calculus Curry-Howard Isomorphism ぼちぼち書いていきます。 ↑
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
サービス終了のお知らせ
