ProofCafe - Coq2Scala
#Coq to Scala English ##概要 Coq2ScalaはCoqのExtraction機能に関する拡張です。 Coq2ScalaはCoqで定義されたアルゴリズムをScalaと連携しJVM上で高速に動作させることを可能にします。 開発者: 今井宜洋(ITプランニング)、姜帆(東京大学 情報理工学系研究科) ハッシュタグ: #coq2scala リポジトリ: http://bitbucket.org/yoshihiro503/coq2scala ##アルゴリズム Mprime_annot ##ダウンロード こちらからパッチをダウンロードできます: https://bitbucket.org/yoshihiro503/coq2scala/downloads ##インストール 1. 上記から差分ファイルをダウンロードし、対応するcoqのソースコードもCoq本家から取得します。 2.
形式手法をプログラミング言語に統合せよ | XCrossOver
この記事の所要時間： 約 2分48秒 Haskell界隈なのかどうかはちょっと微妙ですが、一部で形式手法に注目が集まっています。 形式手法自体はBメソッドやVDMなど昔からあるのですが、最近注目されているのは、CoqとAlloyです。 Coqは熱狂的な盛り上がりを見せているようですが、如何せん書物が追いついていないようです。 Alloyは日本語訳された書籍が販売されています。 Amazon.co.jp： 抽象によるソフトウェア設計－Alloyではじめる形式手法－: Daniel Jackson, 中島 震, 今井 健男, 酒井 政裕, 遠藤 侑介, 片岡 欣夫: 本 これを読んでいてふと思ったのが、形式手法は形式手法、プログラムはプログラムと棲み分ける時代はもう終わったのではないか、ということです。 特にCoqでは、証明駆動開発などというものも考えられていて、 Coqによる証明駆動開発
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
