Coqで、クイックソート - にわとり小屋でのプログラミング
（＊ 注意：今回はCoq 8.1以上を使用。 ＊） 今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。 Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では、明らかに停止する構造を持つ必要がある。 Coqでは、必ず停止する関数のみが定義できる、という制限のため、このように再帰する関数を定義するのは難しいが、Coqで作った関数は、必ず停止して結果を返す、という性質を保っている。 しかし、Fixpointによる定義では、簡単に定義できない再帰関数もある。 例えば、次のように、クイックソートの関数を素直にかいてみると、以下のようなエラーになる。 (* クイックソートの定義 失敗例 *) Fixpoint qsort (l : list A) : list A := mat
本当にTodoリストを活用するための正しいTodoリストの作り方 | ライフハッカー・ジャパン
Todoリストを作ったことのある人ならば、それを完ぺきに終わらせる難しさもご存知ですよね。しかしそれは、Todoリストを正しく作れていないのが原因かもしれません。心理学系ブログ「Psychology Today」のKathleen McGowan氏の記事によると、Todoリストには正しい作り方と間違った作り方があるそうです。 間違ったTodoリストの作り方というのは、どういうものなのでしょうか？ Todoリストを見ると、実際の仕事の内容だけが書いてありますが、実は「Todoリストを作る」ことをやり終えると、それだけで何か仕事をしたような気分になります。それはある意味、Todoリストに書いてある本当の仕事を、先延ばしにしているだけなのです。 実際の仕事を効率よく進めるために必要なはずのTodoリスト作りが、単に仕事を遅らせることになっているなんて、本末転倒ですよね。では、正しいTodoリスト
Getting started
The Coq Proof Assistant A Tutorial Version 1 Gérard Huet, Gilles Kahn and Christine Paulin-Mohring LogiCal Project 1This research was partly supported by IST working group “Types” Getting started Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs
Coq for POPL folk
Using Proof Assistants for Programming Language Research or, How to write your next POPL paper in Coq San Francisco, CA January 8th, 2008 A tutorial on the use of the Coq proof assistant in formalizing programming language metatheory. This tutorial will be tailored to people who are familiar with syntactic proofs of programming language metatheory, such as type soundness, but have never used a pro
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
MUSIC PAINTING - Glocal Sound - Matteo Negrin
- visit Matteo Negrin's site at: http://www.myspace.com/matteonegrin - buy Matteo Negrin's CD at : http://www.jazzos.com/ VIDEO - MUSIC PAINTING created by Smile Lab (info.smilelab@gmail.com) http://vimeo.com/user5512945 Alice Ninni Alberto Filippini Luca Cattaneo © and property of Matteo Negrin and Smile Lab
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Coqによる証明駆動開発