Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory.
This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.
Author(s): Yves Bertot, Pierre Castéran
Series: Texts in Theoretical Computer Science An EATCS Series
Publisher: Springer
Year: 2004
Language: English
Pages: 491
Tags: Software Engineering/Programming and Operating Systems; Computer System Implementation; Programming Techniques; Software Engineering; Logics and Meanings of Programs; Artificial Intelligence (incl. Robotics)
Front Matter....Pages I-XXV
A Brief Overview....Pages 1-11
Types and Expressions....Pages 13-42
Propositions and Proofs....Pages 43-72
Dependent Products or Pandora’s Box....Pages 73-103
Everyday Logic....Pages 105-135
Inductive Data Types....Pages 137-186
Tactics and Automation....Pages 187-210
Inductive Predicates....Pages 211-250
* Functions and Their Specifications....Pages 251-284
* Extraction and Imperative Programming....Pages 285-307
* A Case Study....Pages 309-324
* The Module System....Pages 325-346
** Infinite Objects and Proofs....Pages 347-376
** Foundations of Inductive Types....Pages 377-406
* General Recursion....Pages 407-432
* Proof by Reflection....Pages 433-448
Back Matter....Pages 449-472
