Spara
Interactive Theorem Proving and Program Development
Författare:
häftad, 2010
Engelska
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.
- Undertitel
- Coq’Art: The Calculus of Inductive Constructions
- Författare
- Yves Bertot, G. Huet, Pierre Castéran, C. Paulin-Mohring
- Upplaga
- Softcover reprint of hardcover 1st ed. 2004
- ISBN
- 9783642058806
- Språk
- Engelska
- Vikt
- 310 gram
- Utgivningsdatum
- 2010-12-15
- Sidor
- 472
