Bertot / Castéran | Interactive Theorem Proving and Program Development | E-Book | sack.de
E-Book

E-Book, Englisch, 472 Seiten, eBook

Reihe: Texts in Theoretical Computer Science. An EATCS Series

Bertot / Castéran Interactive Theorem Proving and Program Development

Coq’Art: The Calculus of Inductive Constructions
2004
ISBN: 978-3-662-07964-5
Verlag: Springer
Format: PDF
 Kopierschutz: 1 - PDF Watermark

Coq’Art: The Calculus of Inductive Constructions

E-Book, Englisch, 472 Seiten, eBook

Reihe: Texts in Theoretical Computer Science. An EATCS Series

ISBN: 978-3-662-07964-5
Verlag: Springer
Format: PDF
 Kopierschutz: 1 - PDF Watermark

A practical introduction to the development of proofs and certified programs using Coq.

An invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.

Bertot / Castéran Interactive Theorem Proving and Program Development jetzt bestellen!

Zielgruppe

Graduate

Autoren/Hrsg.

Bertot, Yves
Castéran, Pierre

Weitere Infos & Material

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.

Ihre Fragen, Wünsche oder Anmerkungen
Vorname*
Nachname*
Ihre E-Mail-Adresse*
Kundennr.
Ihre Nachricht*
Lediglich mit * gekennzeichnete Felder sind Pflichtfelder.
Wenn Sie die im Kontaktformular eingegebenen Daten durch Klick auf den nachfolgenden Button übersenden, erklären Sie sich damit einverstanden, dass wir Ihr Angaben für die Beantwortung Ihrer Anfrage verwenden. Selbstverständlich werden Ihre Daten vertraulich behandelt und nicht an Dritte weitergegeben. Sie können der Verwendung Ihrer Daten jederzeit widersprechen. Das Datenhandling bei Sack Fachmedien erklären wir Ihnen in unserer Datenschutzerklärung.