はじめてのCoq

なぜ、開発は人間によって担われているのか？　（pdf）

参考資料

• IT技術とCoqの世界 –証明 = プログラム = 計算の意味を考える
• ソフトウェア・エンジニアリングの新しい潮流 — Deep Specificationの世界 
• AWSでの形式手法の利用　

MaruLabo Hands on はじめてのCoq

Coqのインストール　

平原ゼミ Coq スタートアップセミナー を利用ください

Hands on のソース

Github https://github.com/maruyama097/coq-tutorial

Hello Coq!

Hello Coq! (1) — Coqとのはじめての対話 (pdf)

Hello Coq! (2) — 人間はCoqに何を伝えたか？ (pdf)

Hello Coq! (3) — Coqは人間に何を伝えたか？ (pdf)

論理式の証明

論理式はどのような形をしているか？( pdf )

論理式の部分式への分解とサブゴール ( pdf )

構成のルールと演繹のルール　( ムービー　pdf )

「正しい」ことと「証明を持つ」こと (  pdf )

命題論理の演繹ルール　( pdf )

Coqの返す「証明の状態」と演繹ルール　( pdf )

tactic (1) サブゴールの形と演繹ルールの選択   ( pdf )

tactic (2) 仮説部の形と演繹ルールの選択  ( pdf )

「否定」について   ( pdf )