Interactive Theorem Proving and Program Development : Coq'Art: The Calculus of Inductive Constructions /
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...
| Main Author: | |
|---|---|
| Corporate Author: | |
| Other Authors: | |
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2004.
|
| Series: | Texts in Theoretical Computer Science An EATCS Series.
|
| Subjects: | |
| Online Access: | Connect to the full text of this electronic book |
Search Result 1