Vor Ort
Merkzettel Warenkorb
  • Produktbild: Interactive Theorem Proving and Program Development
  • Produktbild: Interactive Theorem Proving and Program Development
- 10%

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

Aus der Reihe Texts in Theoretical Computer Science. An EATCS Series
10% sparen

114,99 € UVP 128,39 €

inkl. gesetzl. MwSt., Versandkostenfrei

Beschreibung

Produktdetails

Einband

Gebundene Ausgabe

Erscheinungsdatum

14.05.2004

Abbildungen

XXV, 472 p. 1 illus.

Verlag

Springer Berlin

Seitenzahl

472

Maße (L/B/H)

24,1/16/3,3 cm

Gewicht

910 g

Auflage

2004

Sprache

Englisch

ISBN

978-3-540-20854-9

Beschreibung

Rezension

From the reviews of the first edition:



"This book serves as a Coq user manual, supporting both beginners and experts in the use of Coq and its underlying theory. … Numerous exercises further enhance the utility as a learning aid. A supporting website provides downloadable source for all the examples and solutions to the exercises. As an introduction to Coq the book is self-contained … . The book is also comprehensive … . In summary, the book is an essential companion for every Coq user … ." (Valentin F. Goranko, Zentralblatt MATH, Vol. 1069, 2005)

Produktdetails

Einband

Gebundene Ausgabe

Erscheinungsdatum

14.05.2004

Abbildungen

XXV, 472 p. 1 illus.

Verlag

Springer Berlin

Seitenzahl

472

Maße (L/B/H)

24,1/16/3,3 cm

Gewicht

910 g

Auflage

2004

Sprache

Englisch

ISBN

978-3-540-20854-9

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: ProductSafety@springernature.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • Produktbild: Interactive Theorem Proving and Program Development
  • Produktbild: Interactive Theorem Proving and Program Development
  • 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.