Texts in Theoretical Computer Science. An EATCS Series

Interactive Theorem Proving and Program Development

Coq’Art: The Calculus of Inductive Constructions

Authors: Bertot, Yves, Castéran, Pierre

Buy this book

eBook 63,06 €
price for Spain (gross)
  • ISBN 978-3-662-07964-5
  • Digitally watermarked, DRM-free
  • Included format: PDF
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Hardcover 77,95 €
price for Spain (gross)
  • ISBN 978-3-540-20854-9
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
  • The final prices may differ from the prices shown due to specifics of VAT rules
Softcover 77,95 €
price for Spain (gross)
  • ISBN 978-3-642-05880-6
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
  • The final prices may differ from the prices shown due to specifics of VAT rules
About this Textbook

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.

Reviews

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)


Table of contents (16 chapters)

Buy this book

eBook 63,06 €
price for Spain (gross)
  • ISBN 978-3-662-07964-5
  • Digitally watermarked, DRM-free
  • Included format: PDF
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Hardcover 77,95 €
price for Spain (gross)
  • ISBN 978-3-540-20854-9
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
  • The final prices may differ from the prices shown due to specifics of VAT rules
Softcover 77,95 €
price for Spain (gross)
  • ISBN 978-3-642-05880-6
  • Free shipping for individuals worldwide
  • Usually dispatched within 3 to 5 business days.
  • The final prices may differ from the prices shown due to specifics of VAT rules
Loading...

Recommended for you

Loading...

Bibliographic Information

Bibliographic Information
Book Title
Interactive Theorem Proving and Program Development
Book Subtitle
Coq’Art: The Calculus of Inductive Constructions
Authors
Series Title
Texts in Theoretical Computer Science. An EATCS Series
Copyright
2004
Publisher
Springer-Verlag Berlin Heidelberg
Copyright Holder
Springer-Verlag Berlin Heidelberg
eBook ISBN
978-3-662-07964-5
DOI
10.1007/978-3-662-07964-5
Hardcover ISBN
978-3-540-20854-9
Softcover ISBN
978-3-642-05880-6
Series ISSN
1862-4499
Edition Number
1
Number of Pages
XXV, 472
Number of Illustrations and Tables
1 b/w illustrations
Topics