ProofCafe - Front PageLogin / Get an account Logout viewedithistorydiscuss Front Page ProofCafe ー 名古屋Coq勉強会 ー の情報は、以下のリンクを参照してください。 https://proofcafe.connpass.com powered by gitit , hosted on proofserver
MessagePack for OCamlを公開しました - みずぴー日記
くえにしさん([twitter:@kuenishi]さん)に誘われたのでMessagePackハッカソンに参加してきました。 MessagePack本体のレポジトリにMessagePack for OCamlを取り込んでもらったので、みんな使ってください! MessagePackって? JSONやYAMLと同程度の表現能力をもった省スペースなオブジェクトシリアライザです。対応言語もC/C++/Java/D/Ruby/Haskellなどと非常に多いです。 対応言語言一覧 → http://wiki.msgpack.org/display/MSGPACK/QuickStart 公式Wikiの採用実績によると、かなりメジャーなプロジェクトも採用されているようです。実際、ハッカソンにも仕事で利用されている方が結構来ていました。 実はボクたちの作っているチャットアプリのAsakusaSatellit
名古屋Reject会議で「証明駆動開発のたのしみ」というタイトルで発表してきました - みずぴー日記
証明駆動開発のたのしみ@名古屋reject会議 View more presentations from Hiroki Mizuno
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
NGK忘年会2010でCoqの紹介をしてきました - みずぴー日記
NGK忘年会2010（昼の部） : ATNDという名古屋の全コミュニティ合同の忘年会に参加してきました。 発表したこと NGK忘年会 2010 / CoqからRubyへView more presentations from mzpi.発表動画@Ustream CoqPartyのスライドの使いまわしです。 Coq楽しいよ、盛り上ってるよ、って話をだらだらしてきました。 Coq入門記事 上のスライドでCoqに興味を持ってくれた人が数人いるらしいので、入門記事へのリンクを貼っておきます。 プログラマのための Coq - zyxwvの日記 ガリク先生の講義資料 浅井先生のゼミ資料 あとProofCafeもよろしくお願いします。 懇親会の感想・メモ Scala座でニアミスした[twitter:@PG_kura]さんとやっと話せた [twitter:@fate_fox]がしっかりしすぎててビビる B
Coq Party - rfなブログ
11/27 に、Coq Partyに参加してきました。 資料などはこちら。 エンジニア・ミーツ・Coq すぐ分かる形式手法 形式手法とは？ 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法 仕様化の正しさは終盤のシステムテストまで分からない 結合テストでバグが「こんにちは！」 手戻りコストがとても大きい V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」 ソフトウェア開発の不具合の半数は上流工程 その半分は下流工程まで見つからない 上流時点で「厳密で、間違い、漏れ、抜け、矛盾の無い仕様」が必要 仕様は自然言語で書かれているため、あいまい or/xor 問題や、if/iff 問題 など 自然言語ではなく、形式的な仕様記述が必要 形式手法 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う 数学ベースの厳密な定義 形式仕様は仕様の記述の形式化 プログラムではな
はてなブログ | 無料ブログを作成しよう
新米と秋刀魚のわた焼き お刺身用の秋刀魚を買いました。1尾250円です 3枚におろして、秋刀魚のわたに酒、味醂、醤油で調味して1時間ほど漬け込み、グリルで焼きました 秋刀魚のわた焼き わたの、苦味が程よくマイルドに調味され、クセになる味わいです 艶やかな新米と一緒に 自家製お漬物 土…
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
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
イベントレポート：「ProofSummit2011」
名古屋Ruby会議で「Coq to Rubyで初める証明駆動開発」というタイトルで発表してきました - みずぴー日記
http://proofcafe.org/
http://staff.aist.go.jp/reynald.affeldt/coqdev/coqdev.tar.gz
ProofSummit2011(仮題) - [PARTAKE]
http://proofcafe.co.cc/cochin/
【トップエスイーチュートリアル】 Coqで学ぶ定理証明入門 | topse.or.jp
partake.in
kitayuta.inspect
http://atnd.org/events/9238
