このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

本編のCoq記事

その他ソフトウェア 論理 リンク まとめ

インストールと「誰も書かない」シリーズ1から5：

  1. WindowsへのCoqのインストール - 檜山正幸のキマイラ飼育記
  2. 誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記
  3. 業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2） - 檜山正幸のキマイラ飼育記
  4. カリー／ハワード対応に親しむ （誰も書かないCoq入門以前 3） - 檜山正幸のキマイラ飼育記
  5. Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4） - 檜山正幸のキマイラ飼育記
  6. こうすればCoqに入門できそうだ （誰も書かないCoq入門以前 5） - 檜山正幸のキマイラ飼育記

その他色々：

  1. 寄り道Coq： exactタクティクと型理論と圏論 - 檜山正幸のキマイラ飼育記
  2. Coqで定理を記述してみる、型クラスとか使って - 檜山正幸のキマイラ飼育記
  3. Coqの型クラスの使い方：バンドル方式とアンバンドル方式 - 檜山正幸のキマイラ飼育記
  4. Coqで半環：アンバンドル方式の例として - 檜山正幸のキマイラ飼育記
  5. 中学レベル代入計算からカリー／ハワード流証明の圏へ - 檜山正幸のキマイラ飼育記
  6. Coq小ネタ：関数の外延的等値性とか - 檜山正幸のキマイラ飼育記
  7. 続・関数の外延的等値性 - 檜山正幸のキマイラ飼育記