Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions

You must be logged in to access this title.

Sign up now

Already a member? Log in

Synopsis

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.

Book details

Edition:
2004
Series:
Texts in Theoretical Computer Science. An EATCS Series
Author:
Yves Bertot, Pierre Castéran
ISBN:
9783662079645
Related ISBNs:
9783540208549
Publisher:
Springer Berlin Heidelberg
Pages:
N/A
Reading age:
Not specified
Includes images:
No
Date of addition:
2022-06-30
Usage restrictions:
Copyright
Copyright date:
2004
Copyright by:
N/A 
Adult content:
No
Language:
English
Categories:
Computers and Internet, Mathematics and Statistics, Nonfiction, Philosophy