ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentationソフトウェアの基礎(beta)¶ 本ドキュメントは実験中のものです。 安定板は http://proofcafe.org/sf/ を参照してください。 epub版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.epub mobi版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.mobi Contents:
Tutorial Materials for Programming Language Research
Getting started: You will need the following software. Coq: Version 8.1 or a later release. Binary and source packages are available from the Coq homepage. Either CoqIDE (comes with Coq) or Proof General. Both provide interactive environments for developing proofs and are easier to work with than Coq's toploop. coq-tutorial.zip, which contains all the Coq files and documentation for this tutorial.
VSTTE 2012 Software Verification Competition - ひとり勉強会
VSTTEという国際会議の開催した「ソフトウェア検証大会」 https://sites.google.com/site/vstte2012/compet 問題文PDF に挑戦していました。48時間で5問の仕様と実装が提示されて、その正しさ、つまり停止性や、配列の範囲外アクセスをしないこと、仕様を満たしていることなどを、なんでも自由なツールを使っていいから検証してみよう！というコンテストです。 というわけで、Coq でやってみて、力尽きました。難しいですね！コードだけ貼り付けておきます（提出はしてない）。 Problem 1 とある bool のソートアルゴリズム。 Coq で書けたので停止性は示されているはず 配列は範囲内であることが証明されている整数でしかアクセスできない依存型なのでアクセスも安全なはず 返値が sorted であることも証明付きの依存型なので大丈夫なはず 元のpermu
[Coq] Monads in Coq
Personal memorandum for studying functional languages, theorem proving, and formal verification. But other topics might be included. Written in Japanese (Shift-JIS Encoding). 社内勉強会でMonad入門の話をして、その時にCoqを用いて説明しました。 あまりHaskellに慣れてないのでCoq使ったんですが、CoqではMonad則を証明する必要があるので、実は寧ろ説明に適していました。 HaskellだとMonad則がなぜ必要なのか示すのが面倒そう（任意の関数、なんてのはQuickCheckでも作れ無さそうな気がする）ですが、CoqではそもそもMonad則を満たすことを示さないと、Monadを使えません。 サンプルコー
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Asai Laboratory, Ochanomizu University
継続計算に対する仮想機械の導出 定理証明系Coqを使った各種継続計算の性質の証明 対称 λ 計算 shift/resetを含む部分評価器の実装 MinCamlコンパイラ，Caml Lightにおけるshift/resetの実装 証明木(ほか)の可視化 お茶大情報科学科の時間割自動作成 『四則演算インタプリタを作ろう！』 四則演算インタープリタをつくりましょう 末尾呼び出し(tail call)と継続渡し形式(Continuation Passing Style) lexer（字句解析器）と parser（構文解析器）の作成 (サンプルコード) 局所変数の導入 関数(closure)の追加 大域脱出(exit)の追加 再帰関数の追加 FelleisenのCオペレータ リストの追加 Promptの導入 control/prompt から shift/reset への拡張 対称 λ 計算 Coq
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
はじめての Coq - zyxwvの日記
Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明するためにどうしたらいいかが書いてあるわけじゃないし。 だって「(a -> b -> c) -> (a -> b) -> a -> c" を証明してみましょう」とか言われても全然やる気にならないじゃん。そんなことを証明するために Coq を使いたいわけじゃない！ そんなわけで、ocaml-nagoya の合宿の機会を利用して id:yoshihiro503 さんと id:suer さんに、Coq をプログラミング言語として使う場合の基本を教えてもらってきました。特に id:yoshihiro503 さんは少なくとも僕から見ると Coq M
fm-forum @ ウィキ
Formal Methods Forum 形式手法について広く深く研究する会です。 勉強会 参考資料Coq勉強資料:Certified Programming with Dependent Types Event-B勉強資料:Slides and Rodin Platform archives of the developments corresponding to chapters of the books Coq Coqインストール Coq参考資料 Certified Programming with Dependent Types関係 Coq命題論理の証明 Coqで数独 SPIN SPINインストール リンク集：関連しそうな話へのリンク集
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
partake.in