IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Formal type theory, autumn 2009
582655: Formal Type Theory (4 cr), autumn 2009 News 2010-05-18 The Spring 2010 Coq project assignment and its sample solution are now available. 2010-04-08 The questions and sample solutions to the March 26th separate exam are now available. 2010-01-10 The results are in. See the final version of the checklist for details of the exercise points. Those who failed, or wish to raise their grade, can
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
Coqで独習するならどのページがいい？と聞かれたときのメモ - 簡潔なQ
Download Coq(英語) ダウンロードしなければ何も始まらない。 Download | The Coq Proof Assistant ちなみにLinuxディストリならcoqideパッケージをインストールするのが吉 Coqの入門記事を書く会 そこそこ体系的な入門サイト 2010-09-02 - ひとり勉強会 2010-09-14 - ひとり勉強会 2010-09-19 - ひとり勉強会 2010-10-12 - ひとり勉強会 Coq 99 練習問題。直観主義論理における有名な証明を一通り解ける。 Functional Programming Memo: [Coq] Coq-99 : Part 1 anarchy proof 練習用サイト。途中から一気に難化するのが問題。 わからなかったら他の人の解答も見られる anarchy proof - Curry-Howard Isomorp
ネタ記録庫/Coq - ocaml-nagoya
定理証明器 Coq でHello, world! (よしひろ) † Coqで "Hello, world!" を標準出力させるのはちょっと難しい。 なぜなら純粋だから。 今回は29行ほどのOCamlの力を借りて実装した。 具体的には次の三つのファイルを作った。 coqstring.v helloworld.v main.ml (29行のOCamlコード) ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリストみたいな感じで定義されている。 (*Coqのスタンダードライブラリより*) Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). Inductive string : Set := | EmptyString : string | String : ascii -> string -> strin
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
Coqの入門記事を書く会 (4) - ひとり勉強会
今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。 英語 言語そのものを浅く/深く眺めていく、という方向のテキスト３つ： Coq in a Hurry 「忙しい人のためのCoq入門」。比較的よくまとまっている気がしました。 Coq Proof Assistant： A Tutorial 本家のチュートリアル Interactive Theorem Proving and Program Development (Coq'Art) Amazon 定番の一冊 講義の素材として作られたチュートリアル達。より具体的な題材での演習付きなので面白いかも： 2nd Asian-Pacific Summer School on Formal Methods Using Proof Assistants for Programming Language Research or, H
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://proofcafe.org/~yoshihiro503/home_ja.html
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation