2008-03-01から1ヶ月間の記事一覧

PPL2008に行ってきた。

Coqでπ計算などで有名なReynald Affeldtさんから、貴重な意見がいただけたり、楽しい話がたくさんあったりで、非常に素晴らしい経験だった。 驚いたこと プログラミング in OCamlでも有名な五十嵐先生のところの研究室では、CALと呼ばれる、小さい証明器を使…

Coqで、クイックソート

(* 注意:今回はCoq 8.1以上を使用。 *)今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では…