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
LEADER 02547nmm a2200409 u 4500
001 EB000688514
003 EBX01000000000000000541596
005 00000000000000.0
007 cr|||||||||||||||||||||
008 140122 ||| eng
020 |a 9783662079645 
100 1 |a Bertot, Yves 
245 0 0 |a Interactive Theorem Proving and Program Development  |h Elektronische Ressource  |b Coq’Art: The Calculus of Inductive Constructions  |c by Yves Bertot, Pierre Castéran 
250 |a 1st ed. 2004 
260 |a Berlin, Heidelberg  |b Springer Berlin Heidelberg  |c 2004, 2004 
300 |a XXV, 472 p. 1 illus  |b online resource 
505 0 |a 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 
653 |a Software engineering 
653 |a Computer programming 
653 |a Mathematical logic 
653 |a Architecture, Computer 
653 |a Mathematical Logic and Foundations 
653 |a Software Engineering/Programming and Operating Systems 
653 |a Logics and Meanings of Programs 
653 |a Programming Techniques 
653 |a Computer System Implementation 
653 |a Software Engineering 
653 |a Computer logic 
700 1 |a Castéran, Pierre  |e [author] 
710 2 |a SpringerLink (Online service) 
041 0 7 |a eng  |2 ISO 639-2 
989 |b SBA  |a Springer Book Archives -2004 
490 0 |a Texts in Theoretical Computer Science. An EATCS Series 
856 |u https://doi.org/10.1007/978-3-662-07964-5?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 511.3 
520 |a 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