本书的主要目标是从实践的角度来理解Coq系统及其基本理论：归纳构造演算。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。本书也尽量分解对话以便读者能够通过纸笔或直接在Coq上对其进行重现。有时，本书会给出一些综合表达式；它们乍看起来让人生畏，但事实上也是在Coq证明辅助工具的帮助下得到的。读者应该在试验时对它们进行分解、修改、了解其结构，并获得一种实际的感受。

Coq是一个用于验证定理的证明是否正确的计算机工具。—在推理和编程方面，Coq的语言都拥有足够强大的能力和表达能力，可以构造简单的项，执行简单的证明，直到建了立完整的理论，学习复杂的算法。

本书的主要目：标是从实践的角度来理解Coq系统及其基本理论。即归纳构造演算。这本书给出了大量的例子，所有这些例子都可以在计算机上执行。从本书配套网站WWW.labri．fr／Perso／～casteran／CoqArl可以下载并执行所有证明的例子，而且还提供了书中200个练习的答案。

这本书是一本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。

1　概述

2　类型和表达式

3　命题和证明

4　依赖积

5　常用逻辑

6　归纳数据类型

7　证明策略和自动化证明

8　归纳谓词

9　函数及其规范

10　程序抽取和命令式程序设计

11　实例分析

12　模块系统

13　无穷对象和证明

14　归纳类型基础

15　一般递归

16　自反证明

附录

参考文献