Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions
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...
Main Authors: | , |
---|---|
Format: | eBook |
Language: | English |
Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
2004, 2004
|
Edition: | 1st ed. 2004 |
Series: | Texts in Theoretical Computer Science. An EATCS Series
|
Subjects: | |
Online Access: | |
Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 1 A Brief Overview
- 2 Types and Expressions
- 3 Propositions and Proofs
- 4 Dependent Products, or Pandora’s Box
- 5 Everyday Logic
- 6 Inductive Data Types
- 7 Tactics and Automation
- 8 Inductive Predicates
- 9* Functions and Their Specifications
- 10 * Extraction and Imperative Programming
- 11 * A Case Study
- 12 * The Module System
- 13 ** Infinite Objects and Proofs
- 14 ** Foundations of Inductive Types
- 15 * General Recursion
- 16 * Proof by Reflection
- Insertion Sort
- References
- Coq and Its Libraries
- Examples from the Book