Cover Image

Interactive Theorem Proving and Program Development : Coq'Art: The Calculus of Inductive Constructions /

Show other versions (1)

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

Bibliographic Details
Main Author: Bertot, Yves
Corporate Author: SpringerLink (Online service)
Other Authors: Castéran, P. (Pierre)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg, 2004.
Series:Texts in Theoretical Computer Science An EATCS Series.
Subjects:
Computer science.
Computer network architectures.
Software engineering.
Logic design.
Artificial intelligence.
Electronic books.
Online Access:Connect to the full text of this electronic book
Table of Contents:
  • A Brief Overview
  • Types and Expressions
  • Propositions and Proofs
  • Dependent Products
  • Everyday Logic
  • Inductive Data Types
  • Tactics and Automation
  • Inductive Predicates
  • Functions and Their Specifications
  • Extraction and Imperative Programming
  • A Case Study
  • The Module System
  • Infinite Objects and Proofs
  • Foundations of Inductive Types
  • General Recursion
  • Proof by Reflection
  • Appendix
  • Index.