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...

Full description

Bibliographic Details

Main Author:	Bertot, Yves
Corporate Author:	SpringerLink (Online service)
Other Authors:	Castéran, P. (Pierre)
Format:	eBook
Language:	English
Published:	Berlin, Heidelberg : Springer Berlin Heidelberg, 2004.
Series:	Texts in Theoretical Computer Science An EATCS Series.
Subjects:	Computer science. Computer network architectures. Software engineering. Logic design. Artificial intelligence. Electronic books.
Online Access:	Connect to the full text of this electronic book