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

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