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...

Full description

Main Authors: Bertot, Yves, Castéran, Pierre (Author)
Corporate Author: SpringerLink (Online service)
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