Tallenna
Interactive Theorem Proving and Program Development
Kirjailija:
nidottu, 2010
englanti
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.
- Alaotsikko
- Coq’Art: The Calculus of Inductive Constructions
- Kirjailija
- Yves Bertot, G. Huet, Pierre Castéran, C. Paulin-Mohring
- Painos
- Softcover reprint of hardcover 1st ed. 2004
- ISBN
- 9783642058806
- Kieli
- englanti
- Paino
- 310 grammaa
- Julkaisupäivä
- 15.12.2010
- Sivumäärä
- 472
