Preface: 前書き
Basics: 関数プログラミングとプログラムの証明
Induction: 帰納法による証明
Lists: 直積、リスト、オプション
Poly: 多相性と高階関数
Tactics: More Basic Tactics
- The apply Tactic
- The apply with Tactic
- The injection and discriminate Tactics
- Using Tactics on Hypotheses
- Varying the Induction Hypothesis
- Unfolding Definitions
- Using destruct on Compound Expressions
- Review
- Additional Exercises
Logic: Coqにおける論理
IndProp: Inductively Defined Propositions
- Inductively Defined Propositions
- Using Evidence in Proofs
- Inductive Relations
- Case Study: Regular Expressions
- Case Study: Improving Reflection
- Additional Exercises
Maps: Total and Partial Maps
ProofObjects: The Curry-Howard Correspondence
- Proof Scripts
- Quantifiers, Implications, Functions
- Programming with Tactics
- Logical Connectives as Inductive Types
- Equality
IndPrinciples: Induction Principles
- Basics
- Polymorphism
- Induction Hypotheses
- More on the induction Tactic
- Induction Principles in Prop
- Formal vs. Informal Proofs by Induction
Rel: 関係の性質
Imp: 単純な命令型プログラム
ImpParser: Coqでの字句解析と構文解析
ImpCEvalFun: An Evaluation Function for Imp
- A Broken Evaluator
- A Step-Indexed Evaluator
- Relational vs. Step-Indexed Evaluation
- Determinism of Evaluation Again
Extraction: Extracting ML from Coq
- Basic Extraction
- Controlling Extraction of Specific Types
- A Complete Example
- Discussion
- Going Further