Coq 是一个用于验证定理的证明是否正确的计算机工具。这些定理可能涉及到普通数学、证明理论或程序验证。 我们的主要目标是从实践的角度来理解Coq 系统及其基本理论：归纳构造演算（the Calculus of Inductive Constructions）。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。我们也尽量分解对话（dialogues）以便读者能够通过纸笔或直接在Coq 上对其进行重现。有时，我们会给出一些综合表达式；它们乍看起来让人生畏，但事实上也是在Coq 证明辅助工具的帮助下得到的。读者应该在试验时对它们进行分解、修改、了解其结构，并获得一种实际的感受。 本书有一个相关网站1，读者可以从该网站下载并执行所有证明的例子。我们也提供了书中200 个练习的答案，以备不时之需。这本书及其网站使用的工具都是2004 年初发布的Coq V82。 用户对Coq 中已证明的定理的信心来自于构造演算（Calculus of Inductive Constructions）的性质。构造演算是一个形式系统。以λ 演算和类型（typing ）的观点来看，它结合了逻辑中的一些最新进展。这个演算的主要性质已在此处给出，因为我们相信结合理论和实践的知识是使用Coq 全部表达能力的一条最好的路径。

译者序 定理证明是数学领域中一个古老的分支，它从公理出发，利用推理规则为定理寻找证明过程。但是，当我们把数学定理的手工证明和日常生活中的演绎推理变成一系列能在计算机上自动进行的符号演算的过程和技术时，定理证明就成为当今软件工程领域中一种非常重要的形式化技术，即定理证明系统。今天，定理证明系统已经被广泛应用于数学定理证明、协议验证以及软硬件的安全特性验证等方面，成为人们解决关键软件系统正确性、可信性的重要方法，也是继模型检测技术之后未来软件工程领域的一个重要发展方向。 为了帮助我国广大科技工作者和学生更好地学习、掌握和应用定理证明系统，我们CEREUS 小组翻译了《交互式定理证明和程序开发—–Coq 的艺术: 归纳构造演算》一书。选择翻译这本书主要基于如下几点考虑： 1. Coq 是目前国际上交互式定理证明领域的主流工具，它基于归纳构造演算，有着强大的数学模型基础和很好的扩展性，并有完整的工具集。 2. Coq 有一支强大的全职研发队伍，支持开源，这对于想学习和使用该系统的读者非常有益。 3. 本书的作者一直从事Coq 的研发，在书中提供了大量的示例和习题，可以帮助读者更快地掌握Coq，并理解Coq 背后的基础理论。 翻译从来就不是一件轻松的事，尤其是这种既有很深的理论高度，又有很强的实践要求的书，翻译难度就更大了。CEREUS 小组能够在一年内完成本书的翻译工作，不仅饱含了小组全体成员的辛勤劳动，也得到了国际学术界许多研究人员的帮助。参与本书翻译工作的是清华大学软件学院CEREUS 小组，其中第1～8 章由刘柳、周旻、张连怡负责；第9 章由王瑞负责；...